About

Static Analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area. The 25th Static Analysis Symposium, SAS 2018, will be held in Freiburg im Breisgau, Germany. Previous symposia were held in New York, Edinburgh, Saint-Malo, Munich, Seattle, Deauville, Venice, Perpignan, Los Angeles, Valencia, Kongens Lyngby, Seoul, London, Verona, San Diego, Madrid, Paris, Santa Barbara, Pisa, Aachen, Glasgow, and Namur.

Topics

The technical program for SAS 2018 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of static analysis, including, but not limited to:

Paper Submission

Submissions can address any programming paradigm including concurrent, constraint, functional, imperative, logic, object-oriented, aspect, multi-core, distributed, and GPU programming. Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. Paper submissions should not exceed 15 pages in Springer's Lecture Notes in Computer Science LNCS format, excluding bibliography and well-marked appendices (we may admit additional pages for the final version). Program Committee members are not required to read the appendices, and thus papers must be intelligible without them.
Submissions are handled online:

SAS 2018 author interface of EasyChair

Artifact Submission

As in previous years, we are encouraging authors to submit a virtual machine image containing any artifacts and evaluations presented in the paper. The goal of the artifact submissions is to strengthen our field's scientific approach to evaluations and reproducibility of results. The virtual machines will be archived on a permanent Static Analysis Symposium website to provide a record of past experiments and tools, allowing future research to better evaluate and contrast existing work. Artifact submission is optional. We accept only virtual machine images that can be processed with Virtual Box.  Details on what to submit and how will be sent to the corresponding authors by mail shortly after the paper submission deadline. The submitted artifacts will be used by the program committee as a secondary evaluation criterion whose sole purpose is to find additional positive arguments for the paper's acceptance. Furthermore, an Artifact Evaluation Committee will assess artifacts and will award an "Artifact Approved" stamps to accepted papers that come with an artifact that allows to reproduce the results presented in the paper. Submissions without artifacts are welcome and will not be penalized.

Important Dates

Radhia Cousot Young Researcher Award

Since 2014, the program committee of each SAS conference selects a paper for the Radhia Cousot Young Researcher Best Paper Award, in memory of Radhia Cousot, and her fundamental contributions to static analysis, as well as being one of the main promoters and organizers of the SAS series of conferences.

Invited Talks

1. •Aws Albarghouthi (University of Wisconsin–Madison, USA)
   
   Program Fairness through the Lens of Formal Methods
   Software has become a powerful arbitrator of a range of significant decisions with far-reaching societal impact---hiring, welfare allocation, prison sentencing, policing and, among many others. With the range and sensitivity of algorithmic decisions expanding by the day, the problem of understanding the nature of program discrimination, bias and fairness is a pressing one. In this talk, I will describe our work on the FairSquare project, in which we are developing program verification and synthesis tools aimed at rigorously characterizing and reasoning about fairness of decision-making programs.
   
   

2. •Zak Kincaid (Princeton University, USA)
   
   Non-linear Invariant Generation via Recurrence Analysis
   In this talk, I will present an overview on recent work on generating non-linear numerical invariants for loops and recursive procedures.  The method is compositional in the sense that it operates by breaking the program into parts, analyzing each part independently, and then combining the results.  The fundamental challenge is to devise an effective method for analyzing the behavior of a loop given the results of analyzing its body.  The key idea is to separate the problem into two: first we approximate the loops dynamics using a system of recurrence relations, and second we symbolically compute (non-linear) closed form solutions for the recurrence relations that can be expressed in the property language of the analysis.
   
   

3. •Ruzica Piskac (Yale University, USA)
   
   New Applications of Software Synthesis: Firewall Repair and Verification of Configuration Files
   In this talk we present a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of their administrators – is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.
   We also show, using verification for configuration files, how to learn specification when the given examples is actually a set of configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools.  In this talk we describe a framework which analyzes data sets of correct configuration files and derives rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.
   
   

4. •Sharon Shoham (Tel Aviv University, Israel)
   
   Verification of Distributed Systems Using First-Order Logic
   Distributed systems underlie more and more applications, making their correctness paramount. However, due to the infinite state space (e.g., unbounded number of nodes, messages) and the complexity of the protocols used, verification of such systems is both undecidable and hard in practice. Proof automation can substantially increase productivity in the formal verification of distributed systems. However, the unpredictability of automated provers in handling quantified formulas presents a major hurdle to the usability of these tools.
   This talk describes a deductive verification approach for distributed systems which produces verification conditions in decidable fragments of first-order logic. Decidability greatly improves the predictability of proof automation, resulting in a more practical verification approach. Furthermore, it facilitates an interactive process, where the user may strengthen or weaken the invariants used for verification based on counterexamples.
   

Invited Tutorials

1. •Roberto Bagnara (University of Parma/BUGSENG, Italy)
   
   The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software
   The MISRA project started in 1990 with the mission of providing world-leading best practice guidelines for the safe and secure application of both embedded control systems and standalone software. MISRA C is a coding standard defining a subset of the C language, initially targeted at the automotive sector, but now adopted across all industry sectors that develop C software in safety- and/or security-critical contexts. In this tutorial, we introduce MISRA C, its role in the development of critical software, especially in embedded systems, its relevance to industry safety standards, as well as the challenges of working with a general-purpose programming language standard that is written in natural language with a slow evolution over the last 40+ years. We also outline the role of static analysis in the automatic checking of compliance with respect to MISRA C, and the role of the MISRA C language subset in enabling a wider application of formal methods to industrial software written in C.
   
   

2. •Ken McMillan (Microsoft Research, USA), Oded Padon (Tel Aviv University, Israel)
   
   Deductive Verification in Decidable Fragments with Ivy
   Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.
   On the other hand, there is a long history of work on *decidable* logics or fragments of logics. Generally speaking, decision procedures for these logics perform more predictably and fail more transparently than provers for undecidable logics. In particular, in the case of a false proof goal, they usually can provide a concrete counter-model to help diagnose the problem. However, decidable logics pose severe limitations on expressiveness, and it is not immediately clear that such logics can be applied to proving complex protocols or systems.
   In this tutorial, we will present a practical approach to using decidable logics to prove complex protocols and systems, based on a tool called Ivy. The approach applies abstraction and modular reasoning techniques to mitigate the expressiveness limitations of decidable fragments. The high-level strategy involves the following ideas:
   * Abstracting infinite-state systems using first-order logic.
   * Carefully controlling quantifier-alternations to ensure decidability.
   * Using modular reasoning principles to decompose a proof into decidable lemmas.
   Experience to date indicates that it is possible to prove safety and liveness properties of complex protocols (e.g., Paxos variants), and also to produce verified low-level implementations, using decidable logics. Moreover, the effort required to structure the proof in this way is more than repaid by greater reliability of proof automation, which significantly reduces the overall verification effort. Better matching human reasoning capabilities to the capabilities of automated provers results in a more stable and predictable formal development process.
   
   

3. •Peter O’Hearn (University College London/Facebook, UK)
   
   Experience developing and deploying a concurrency analysis at Facebook
   At the start of 2016 I decided to work on a risky project, the aims of which I had described the year before in an interview with Mike Hicks (http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/)
   “I still want to understand concurrency, scalably. I would like to have analyses that I could deploy with high speed and low friction (e.g., not copious annotations or proof hints) and produce high-quality reports useful to programmers writing concurrent programs without disturbing their workflow too much. Then it could scale to many programmers and many programs. Maybe I am asking for too much, but that is what I would like to find.”
   The project went much better than I had ever hoped. Fast forward to 2018, and the RacerD race detector has found thousands of race bugs which have been fixed by Facebook programmers before code reaches production, it has been instrumental in the conversion of Facebook’s Android App from a single-threaded to a multi-threaded architecture, and it even has received press attention (e.g., in infoq, techrepublic, thenewstack, and elsewhere).
   In this talk I will tell you about the development of the project, its twists and its turns, the compromises and design decisions we made to achieve an impactful analysis, and how jumping back and forth between the perspective of an engineer and that of a scientist helped. My aim is to convey what it’s like to work on an open research problem in static analysis, while at the same time pursuing the industrial goal of helping people, and how these two activities can boost one another.
   

Affiliated Events

1. 
   

2. •9th Workshop on Static Analysis and Systems Biology (SASB 2018)
       Chairs: Tatjana Petrov (University of Konstanz, Germany) and Ankit Gupta (ETH Zurich, Switzerland)
   

3. •9th Workshop on Tools for Automatic Program Analysis (TAPAS 2018)
   

4.      Chair: Fausto Spoto (University of Verona/Julia Srl, Italy)
   

Organization

1. Program Chair
   

2. •Andreas Podelski (University of Freiburg, Germany)
   

1. Program Committee
   

2. •Domagoj Babic (Google Inc., USA)
   

3. •Sam Blackshear (Facebook, USA)
   

4. •Marc Brockschmidt (Microsoft Research, UK)
   

5. •Swarat Chaudhuri (Rice University, USA)
   

6. •Bor-Yuh Evan Chang (University of Colorado Boulder, USA)
   

7. •Jérôme Feret (INRIA/ENS/CNRS, France)
   

8. •Ashutosh Gupta (TIFR, India)
   

9. •Nicolas Halbwachs (Verimag/CNRS, France)
   

10. •Lukáš Holík (Brno University of Technology, Czech Republic)
    

11. •Barbara König (University of Duisburg-Essen, Germany)
    

12. •Boris Köpf (IMDEA Software Institute, Spain)
    

13. •Shuvendu Lahiri (Microsoft Research, USA)
    

14. •Hakjoo Oh (Korea University, South Korea)
    

15. •Sylvie Putot (École Polytechnique, France)
    

16. •Francesco Ranzato (University of Padova, Italy)
    

17. •Jakob Rehof (TU Dortmund University, Germany)
    

18. •Xavier Rival (CNRS/ENS/INRIA, France)
    

19. •Sriram Sankaranarayanan (University of Colorado Boulder, USA)
    

20. •Harald Søndergaard (The University of Melbourne, Australia)
    

21. •Alexander J. Summers (ETH Zurich, Switzerland)
    

22. •Ashish Tiwari (SRI International, USA)
    

23. •Caterina Urban (ETH Zurich, Switzerland)
    

24. •Lenore Zuck (University of Illinois at Chicago, USA)
    

25. •Damien Zufferey (MPI-SWS, Germany)
    

26. •Florian Zuleger (TU Wien, Austria)
    

1. Artifact Evaluation Chair
   

2. •Xavier Rival (CNRS/ENS/INRIA, France)
   

1. Artifact Evaluation Committee
   

2. •Ahmad Salim Al Sibahi (University of Copenhagen, Denmark)
   

3. •Frédéric Besson (Inria/Univ Rennes/CNRS/IRISA, France)
   

4. •Liqian Chen (NUDT, China)
   

5. •Gidon Ernst (National Institute of Informatics, Japan)
   

6. •George Fourtounis (University of Athens, Greece)
   

7. •Kihong Heo (University of Pennsylvania, USA)
   

8. •Huisong Li (CNRS/ENS/INRIA, France)
   

9. •Sergio Mover (University of Colorado Boulder, USA)
   

10. •Hakjoo Oh (Korea University, South Korea)
    

11. •Oded Padon (Tel Aviv University, Israel)
    

12. •Jihyeok Park (KAIST, South Korea)
    

13. •Marie Pelleau (University Nice/Sophia Antipolis, France)
    

14. •Markus Schordan (Lawrence Livermore National Laboratory, USA)
    

15. •Fausto Spoto (University of Verona/Julia Srl, Italy)
    

16. •David Sprunger (National Institute of Informatics, Japan)
    

17. •Caterina Urban (ETH Zurich, Switzerland)
    

18. •Jules Villard (Facebook)
    

1. Publicity Chair
   

2. •Caterina Urban (ETH Zurich, Switzerland)
   

Sponsors

1. 
   

2. 

   
   
3. 

   
   
4. 

   
   
5.