Semper

The goal of the Semper project is to build an automatic program verifier for Scala programs. Some of the key research challenges that we are currently exploring are: (1) how to automatically verify concurrent programs that make use of a variety of idioms, in particular, actors; (2) how to effectively reduce the annotation overhead by integrating the verifier with a powerful contract inference; and (3) how to reason about the functional features of Scala such as closures using automatic theorem provers.

The verification methodology used in Semper is based on Chalice. The inference is performed by our generic abstract interpreter Sample, which can be instantiated with various custom analyses.

Key Results

Semper is a new project. Initial results include a verification methodology for closures, a new specification methodology based on fractional permissions, static analyses for pattern matching, information flow, and string values, and an automatic inference of access permissions.

Publications

• I. T. Kassios and E. Kritikos: A Discipline for Program Verication based on Backpointers and its Use in Observational Disjointness To appear in European Symposium of Programming (ESOP) 2013. [PDF] [BIB]
• I. T. Kassios and P. Müller and M. Schwerhoff: Comparing Verification Condition Generation with Symbolic Execution: an Experience Report
  Verified Software Theories Tools Experiments (VSTTE), 2012. [PDF][BIB]
• M. Zanioli and P. Ferrara and A. Cortesi: SAILS: static analysis of information leakage with Sample
  ACM Symposium on Applied Computing (SAC), 2012. [PDF] [BIB]
• P. Ferrara and P. Müller: Automatic inference of access permissions
  Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012. [PDF] [BIB] Springer-Online
• G. Costantini and P. Ferrara and A. Cortesi: Static Analysis of String Values
  International Conference on Formal Engineering Methods (ICFEM), 2011. [PDF] [BIB] Springer-Online
• S. Heule and K. R. M. Leino and P. Müller and A. J. Summers: Fractional Permissions Without the Fractions
  Formal Techniques for Java-like Programs (FTfJP),2011. [PDF] [BIB]
• P. Ferrara: Static Type Analysis of Pattern Matching by Abstract Interpretation
  Formal Techniques for Distributed Systems (FMOODS/FORTE),2010. [PDF] [BIB] Springer-Online
• I. T. Kassios and P. Müller: Specification and Verification of Closures
  Technical Report, ETH Zurich, 2010. [PDF] [BIB]

Collaboration

We collaborate with the group of Tino Cortesi, Universita` Ca' Foscari, Venezia, on static analysis.

Project Members at ETH

Pietro Ferrara
Uri Juhasz
Ioannis Kassios
Peter Müller
Milos Novacek
Malte Schwerhoff
Alex Summers

Funding

Our work on Semper is partly funded by the Hasler Foundation and the Swiss National Science Foundation SNF.