No.063 Semantics and Verification of Object-Oriented Languages

Icon

NII Shonan Meeting Seminar 063

Organizers

  • Atsushi Igarashi, Kyoto University, Japan
  • Andrzej Murawski, University of Warwick, United Kingdom
  • Nikos Tzevelekos, Queen Mary University of London, United Kingdom

Participants

  • Davide Ancona
  • Tomoyuki Aotani
  • Werner Dietl
  • Atsushi Igarashi
  • Vasileios Koutavas
  • Gary T. Leavens
  • Rustan Leino
  • Xin Li
  • Nadia Polikarpova
  • Erik Poll
  • Alex Potanin
  • Steven Ramsay
  • Julian Rathke
  • Sukyoung Ryu
  • Alex Summers
  • Tachio Terauchi
  • Nikos Tzevelekos
  • Hiroshi Unno
  • Thomas Wies
  • Hongseok Yang

Schedule

20th September, 2015

  • 15:00- Hotel Check In
  • 19:00-21:00: Welcome Reception

21st September, 2015

  • 7:30-9:00: Breakfast
  • 9:00-10:30: Technical Session
    • Self-introduction by participants
  • 10:30-11:00: Break
  • 11:00-11:45: Technical Session
    • Werner Dietl:?Collaborative Verification of the Information Flow for a
      High-Assurance App Store
  • 12:00-13:30: Lunch
  • 13:30-14:00: Group Photo Shooting
  • 14:00-15:30: Technical Session
    • Thomas Wies: Automating Separation Logic using SMT
  • 15:00-15:30: Break
  • 15:30-17:00: Technical Session
    • Hiroshi Unno: Verification of Featherweight Java Programs via
      Transformation to Higher-order Functional Programs with Recursive Data Types
    • Xin Li: Automata-Based Abstraction Refinement for muHORS Model
  • 18:00-19:30: Dinner

22nd September, 2015

  • 7:30-9:00: Breakfast
  • 9:00-10:00: Technical Session
    • Werner Dietl: Tutorial on the Checker framework
  • 10:00-10:30: Break
  • 10:30-12:00: Technical Session
    • Nadia Polikarpova: A Fully Verified Container Library
    • Sukyoung Ryu: Analyzing JavaScript Web Applications in the Wild (Mostly)
      Statically
  • 12:00-13:30: Lunch
  • 13:30-15:00: Technical Session
    • Hongseok Yang: ‘Cause I’m Strong Enough’: Reasoning about Consistency
      Choices in Distributed Systems
    • Gary Leavens: Modular Reasoning and a Definition of Supertype Abstraction
  • 15:00-15:30: Break
  • 15:30-17:00: Technical Session
    • Erik Poll: State machine learning: from testing to formal specifications
    • Tachio Terauchi: On predicate refinement heuristics used in CEGAR
  • 18:00-19:30: Dinner

23rd September, 2015

  • 7:30-9:00: Breakfast
  • 9:00-10:00: Technical Session
    • Davide Ancona: Type soundness proofs with big-step operational semantics of
      object-oriented languages
  • 10:00-10:30: Break
  • 10:30-12:00: Technical Session
    • Atsushi Igarashi: Type Systems for Dynamic Layer Composition
    • Tomoyuki Aotani: A semantics for context-oriented programming languages with?multiple layer activation mechanisms
  • 12:00-13:30: Lunch
  • 13:30-15:00: Technical Session
    • Nikos Tzevelekos: Game Semantics for Interface Middleweight Java
    • Steven Ramsay: Deciding contextual equivalence for IMJ*
  • 15:00-15:30: Break
  • 15:30-16:15: Technical Session
    • Vassilis Koutavas: Reasoning about Class Behavior using the Bisimulation Technique
  • 18:00-19:30: Dinner

24th September, 2015

  • 7:30-9:00: Breakfast
  • 9:00-10:00: Technical Session
    • Alex Summers: The Viper Project: Verification Infrastructure for?Permission-based Reasoning
  • 10:00-10:30: Break
  • 10:30-12:00: Technical Session
    • Alex Potanin: Wyvern Formalisation: Objects, Classes, Modules, and Type Members
    • Rustan Leino: Traits and dynamic frames
  • 12:00-13:30: Lunch
  • 13:30- Excursion to Kamakura and Banquet

25th September, 2015

  • 7:30-9:00: Breakfast
  • 9:00-10:00: Technical Session
    • TBD
  • 10:00-10:30: Break
  • 10:30-12:00: Technical Session
    • TBD
  • 12:00-13:30: Lunch

Overview

Motivation
Software applications are increasingly often desired, or even required, to come with guarantees as to their performance, correctness and reliability. Such guarantees have typically been of focal importance to safety-critical applications such as avionics, automotive systems and nuclear reactor controllers. Nowadays, with software being pervasive and having a key role in our daily lifestyles, the focus of the game has greatly broadened. Verified code has become a desideratum of software development in general: it concerns widespread applications written in mainstream languages. The verification problem for such languages poses new challenges as high-level programming features (references, objects, classes, etc.) need to be handled accurately. Moreover, realistic applications can expand to million lines of code, thus demanding accurate but scalable methods. Taking these parameters into account, we herewith propose a seminar devoted to modelling and verifying object-oriented code. The aim of the meeting will be to take stock of the present situation, to foster communication between researchers pursuing diverse approaches and to propose challenges for the future.

The object-oriented paradigm has been embraced by mainstream software companies as well as academic curricula. It has also been gaining ground in verification. Although, traditionally, verification has been conducted for constrained but technically robust programming languages, time has shown that there is a need to loosen the constraints in order to make comprehensive impact. Everyday software development primarily concerns mainstream languages, which provide a range of expressive features, greatly enhancing the development and maintenance of code. Moreover, they also attract a good supply of skilful developers. On the object-oriented front, Java has become widespread and the trend is complemented by the development of C# and Scala. Each of them offers safety compile-time and run-time checks, which are not present in other competitors like C/C++. They emerge as the natural choices to target with modelling and verification techniques, if one is interested in the analysis of safe object-oriented programs. Many efforts have been dedicated in recent years to provide techniques to address the issue. The vision of dependable/verified software has become the driving force behind numerous research projects in the UK and inspired one of the official UK CRC Grand Challenges for the next decade. The formal verification of object-oriented software has also been the subject of international initiatives, such as the European Concerted Research Action IC0701.

Object-oriented code presents a whole variety of interesting technical challenges, stemming from the fact that it involves a unique combination of more general computational concepts, such as recursive types, higher-order references, self-reference, state encapsulation, polymorphism etc. Each of them is a challenge in its own right and over the years dedicated research programmes have been developed to understand the features in isolation. The proposed seminar will provide a forum in which such neighbouring fields can be discussed from the point of view of object-oriented languages. We hope to identify opportunities for transfers of techniques with a view to specializing them to the specific setting of object-oriented code. As well as assessing the more established lines of work in the area, we will also aim to predict new fruitful directions, emerging from the constant evolution of OO-languages, the addition of new features, capabilities and structuring constructs.

Semantics of OO Languages
Formal analysis of object-oriented code has been the subject of extensive research [3]. A substantial part of this effort concentrated on the analysis of type systems and their safety. Significant progress was enabled by the definition of simple object calculi, such as Featherweight [16] and Middleweight Java [6], which capture the essentials of crucial aspects of Java in a compact setting, much more amenable to formal analysis.

Java was also analysed through denotational semantics [11, 25, 23], trace semantics [17, 30] and bisimulations [18]. These provide methods for reasoning about contextual equivalences, be it for programs, classes or packages. Bisimulations are well-suited to underpin mechanized reasoning, while game models open up the way to compositional and automated analysis in combination with automata theory [2]. There is also a significant body of work on specification languages [10] and program logics [1, 27], reinvigorated recently through advances in modular reasoning about Java with separation logic [12].

Object generation and maintenance are challenging to accommodate by automata theory, because unbounded entities (e.g. object reference names) need to be managed. To allow one to move between the unbounded and finite, researchers have considered various restrictions, allowing one to pass from the infinite to the finite [4, 29, 26]. There is also a wealth of work in automata over infinite alphabets, developed in connection with database theory [28], which has the potential to inspire future work on objects.

Verification Tools
The advances in semantic modelling of object-oriented programs have in many cases been complemented by the construction of tools for a variety of verification tasks. In some cases, scalability to industrial-size software has been achieved.

Java Pathfinder (JPF) [15] is a tool developed at the NASA Ames Research Center for verifying Java bytecode. It is an explicit state model-checker that, leaning upon abstractions and optimizations, has been successful in tackling industrial code [24], including NASA’s K9 Rover Executive subsystem [14]. It is arguably the most successful approach to verifying Java code.

The Java Modelling Language (JML) [8] underpins several other tools. It is a specification language for Java programs that follows the design by contract paradigm. ESC/Java [19] (and more recently ESC/Java2 [10]) can detect common run-time errors through extented static checking [13], which involves the use of JML and a theorem prover. The ESC/Java approach is neither sound nor complete. Krakatoa [22] is a JML-based tool that does guarantee soundness.

Boogie [21] is an intermediate verification language on top of which there have been built verifiers for several languages, including Spec# [5]. More recently, researchers working on separation-logic-based techniques have developed jStar, a tool for analysing Java code [12], which combines separation logic with bi-abduction [9] to achieve compositional analysis. That work has been extended to coreStar [7], which aims to provide a general framework for modular verification.

A seminar to bring together experts on diverse approaches
Object-oriented programs have been approached from a multitude of directions: automata theory, model checking, semantics, types, verification tools and others. This variety suggests not only that the problem is an interesting and challenging one but also that there is space for technology exchange and cross-fertilisation between different approaches. This is precisely the target of the proposed seminar. Accordingly, we have compiled a list of participants representing all the diverse approaches and traditions of work.

References
[1] M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Verification: Theory and Practice, volume 2772 of Lecture Notes in Computer Science, pages 11?41. Springer, 2003.
[2] S. Abramsky, D. R. Ghica, A. S. Murawski, and C.-H. L. Ong. Applying game semantics to compositional software modelling and verification. In Proceedings of TACAS, volume 2988 of Lecture Notes in Computer Science, pages 421?435. Springer-Verlag, 2004.
[3] Jim Alves-Foss, editor. Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science. Springer, 1999.
[4] M. Faouzi Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. 00111, 7(4), 2011.
[5] Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, volume 4111 of Lecture Notes in Computer Science, pages 364?387, 2005.
[6] G.M. Bierman, M.J. Parkinson, and A.M. Pitts.
MJ: An imperative core calculus for Java and Java with effects. Technical Report Technical Report 563, Computer Laboratory, University of Cambridge, 2002.
[7] Matko Botincan, Dino Distefano, Mike Dodds, Radu Grigore, Daiva Naudziuniene, and Matthew J Parkinson. corestar: The core of jStar. In Boogie’11: 1st International Workshop on Intermediate Verification Languages, 2011.
[8] L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7(3):212?232, 2005.
[9] Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26, 2011.
[10] P. Chalin, J. R. Kiniry, G. T. Leavens, and E. Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In FMCO, volume 4111 of Lecture Notes in Computer Science, pages 342?363. Springer, 2005.
[11] W. R. Cook and J. Palsberg. A denotational semantics of inheritance and its correctness. In OOPSLA, pages 433?443. ACM, 1989.
[12] D. Distefano and M. J. Parkinson. jStar: towards practical verification for Java. In OOPSLA, pages 213?226. ACM, 2008.
[13] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R Stata. Extended static checking for Java. In PLDI, pages 234?245, 2002.
[14] D. Giannakopoulou, C.S. Pasareanu, M. Lowry, and R. Washington. Lifecycle verification of the NASA Ames K9 Rover Executive. In ICAPS’05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Sys- tems (VVPS’05), 2005.
[15] K. Havelund and T. Pressburger. Model checking Java programs using Java Pathfinder. International Journal on Software Tools for Technology Transfer, 2(4):366?381, 2000.
[16] A. Igarashi, B. C. Pierce, and P. Wadler. Feather-weight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396?450, 2001.
[17] A. Jeffrey and J. Rathke. Java Jr: Fully abstract trace semantics for a core Java language. In Proceedings of ESOP, volume 3444 of Lecture Notes in Computer Science, pages 423?438. Springer, 2003.
[18] V. Koutavas and M. Wand. Reasoning about class behavior. In Proceedings of FOOL/WOOD. 2007.
[19] K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java User’s Manual SRC Technical Note 2000-002.
[20] Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, and Bart Jacobs. Jml (poster session): notations and tools supporting detailed design in java. In OOPSLA Addendum, pages 105?106, 2000.
[21] K. Rustan M. Leino. This is Boogie 2. Technical report, Microsoft Research, 2008.
[22] C. March´e, C. Paulin-Mohring, and X. Urbain. The krakatoa tool for certification of Java/Java Card programs annotated in jml. J. Log. Algebr. Program., 58(1-2):89?106, 2004.
[23] A. S. Murawski and N. Tzevelekos. Game semantics for Interface Middleweight Java. In POPL, pages 517?528, 2014.
[24] Corina S. Pasareanu. Combining model checking and symbolic execution for software testing. In TAP, volume 7305 of Lecture Notes in Computer Science, page 2, 2012.
[25] Uday S. Reddy. Objects and classes in Algol-like languages. Information and Computation, 172:63?97, 2002.
[26] J. Rot, F. S. de Boer, and M. M. Bonsangue. Unbounded allocation in bounded heaps. In FSEN, volume 8161 of Lecture Notes in Computer Science, pages 1?16. Springer, 2013.
[27] Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. Nested hoare triples and frame rules for higher-order store. Logical Methods in Computer Science, 7(3), 2011.
[28] L. Segoufin. Automata and logics for words and trees over an infinite alphabet. In Proceedings of CSL, volume 4207 of Lecture Notes in Computer Science. Springer, 2006.
[29] N. Tzevelekos. Fresh-register automata. In Proceedings of POPL, pages 295?306. ACM Press, 2011.
[30] Yannick Welsch and Arnd Poetzsch-Heffter. Full abstraction at package boundaries of object-oriented languages. In SBMF, volume 7021 of Lecture Notes in Computer Science, pages 28?43, 2011.