Visible to the public SAS 2018Conflict Detection Enabled

Submitted by Anonymous on Wed, 03/21/2018 - 11:16am
Aug 29, 2018 7:00 am - Aug 31, 2018 6:00 pm CEST

25th Static Analysis Symposium (SAS 2018)

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

  • Abstract domains
  • Automated deduction
  • Debugging
  • Emerging applications
  • Program optimizations and transformations
  • Program verification
  • Tool environments and architectures
  • Type checking
  • Abstract interpretation
  • Data flow analysis
  • Deductive methods
  • Model checking
  • Program synthesis
  • Security analysis
  • Theoretical frameworks

Invited Talks

Program Fairness through the Lens of Formal Methods
Aws Albarghouthi (University of Wisconsin-Madison, USA)

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.

Non-linear Invariant Generation via Recurrence Analysis
Zak Kincaid (Princeton University, USA)

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.

New Applications of Software Synthesis: Firewall Repair and Verification of Configuration Files
Ruzica Piskac (Yale University, USA)

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.

Verification of Distributed Systems Using First-Order Logic
Sharon Shoham (Tel Aviv University, Israel)

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

The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software
Roberto Bagnara (University of Parma/BUGSENG, Italy)

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.

Ivy: Safety Verification by Interactive Generalization
Ken McMillan (Microsoft Research, USA), Oded Padon (Tel Aviv University, Israel)

Experience developing and deploying a concurrency analysis at Facebook
Peter O'Hearn (University College London/Facebook, UK)

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

  • 9th Workshop on Static Analysis and Systems Biology (SASB 2018)
    Chairs: Tatjana Petrov (University of Konstanz, Germany) and Ankit Gupta (ETH Zurich, Switzerland)
  • 9th Workshop on Tools for Automatic Program Analysis (TAPAS 2018)
    Chair: Fausto Spoto (University of Verona/Julia Srl, Italy)

Organization

Program Chair

  • Andreas Podelski (University of Freiburg, Germany)

Program Committee

  • Domagoj Babic (Google Inc., USA)
  • Sam Blackshear (Facebook, USA)
  • Marc Brockschmidt (Microsoft Research, UK)
  • Swarat Chaudhuri (Rice University, USA)
  • Bor-Yuh Evan Chang (University of Colorado Boulder, USA)
  • Jerome Feret (INRIA/ENS/CNRS, France)
  • Ashutosh Gupta (TIFR, India)
  • Nicolas Halbwachs (Verimag/CNRS, France)
  • Lukas Holik (Brno University of Technology, Czech Republic)
  • Barbara Konig (University of Duisburg-Essen, Germany)
  • Boris Kopf (IMDEA Software Institute, Spain)
  • Shuvendu Lahiri (Microsoft Research, USA)
  • Hakjoo Oh (Korea University, South Korea)
  • Sylvie Putot (Ecole Polytechnique, France)
  • Francesco Ranzato (University of Padova, Italy)
  • Jakob Rehof (TU Dortmund University, Germany)
  • Xavier Rival (CNRS/ENS/INRIA, France)
  • Sriram Sankaranarayanan (University of Colorado Boulder, USA)
  • Harald Sondergaard (The University of Melbourne, Australia)
  • Alexander J. Summers (ETH Zurich, Switzerland)
  • Ashish Tiwari (SRI International, USA)
  • Caterina Urban (ETH Zurich, Switzerland)
  • Lenore Zuck (University of Illinois at Chicago, USA)
  • Damien Zufferey (MPI-SWS, Germany)
  • Florian Zuleger (TU Wien, Austria)

Artifact Evaluation Chair

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

Artifact Evaluation Committee

  • Ahmad Salim Al Sibahi (University of Copenhagen, Denmark)
  • Frederic Besson (Inria/Univ Rennes/CNRS/IRISA, France)
  • Liqian Chen (NUDT, China)
  • Gidon Ernst (National Institute of Informatics, Japan)
  • George Fourtounis (University of Athens, Greece)
  • Kihong Heo (University of Pennsylvania, USA)
  • Huisong Li (CNRS/ENS/INRIA, France)
  • Sergio Mover (University of Colorado Boulder, USA)
  • Hakjoo Oh (Korea University, South Korea)
  • Oded Padon (Tel Aviv University, Israel)
  • Jihyeok Park (KAIST, South Korea)
  • Marie Pelleau (University Nice/Sophia Antipolis, France)
  • Xavier Rival (CNRS/ENS/INRIA, France, Chair of the Artifact Evaluation Committee)
  • Markus Schordan (Lawrence Livermore National Laboratory, USA)
  • Fausto Spoto (University of Verona/Julia Srl, Italy)
  • David Sprunger (National Institute of Informatics, Japan)
  • Caterina Urban (ETH Zurich, Switzerland)
  • Jules Villard (Facebook)

Publicity Chair

  • Caterina Urban (ETH Zurich, Switzerland)
Event Details
Location: 
Freiburg im Breisgau, Germany
URL: 
http://staticanalysis.org/sas2018