title: CVC: A Cooperating Validity Checker

authors:
Aaron Stump
Clark W. Barrett
David L. Dill


venue: cav

title: Evidence-Based Model Checking

authors:
Li Tan
Rance Cleaveland


title: Infinite Games and Verification (Extended Abstract of a Tutorial)


title: Automatic Derivation of Timing Constraints by Failure Analysis

authors:
Tomohiro Yoneda
Tomoya Kitai
Chris J. Myers


title: Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling

authors:
Håkan L. S. Younes
Reid G. Simmons


title: The Quest for Efficient Boolean Satisfiability Solvers

authors:
Lintao Zhang
Sharad Malik


title: Algorithmic Improvements in Regular Model Checking

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Marcus Nilsson
Julien d'Orso


title: Strengthening Invariants by Symbolic Consistency Testing

authors:
Husam Abu-Haimed
Sergey Berezin
David L. Dill


title: Modular Strategies for Infinite Games on Recursive Graphs

authors:
Rajeev Alur
Salvatore La Torre
P. Madhusudan


title: Enhanced Vacuity Detection in Linear Temporal Logic

authors:
Roy Armoni
Limor Fix
Alon Flaisher
Orna Grumberg
Nir Piterman
Andreas Tiemeyer
Moshe Y. Vardi


title: FAST: Fast Acceleration of Symbolikc Transition Systems

authors:
Sébastien Bardin
Alain Finkel
Jérôme Leroux
Laure Petrucci


title: Efficient Image Computation in Infinite State Model Checking

authors:
Constantinos Bartzis
Tevfik Bultan


title: To Store or Not to Store

authors:
Gerd Behrmann
Kim Guldstrand Larsen
Radek Pelánek


title: Rabbit: A Tool for BDD-Based Verification of Real-Time Systems

authors:
Dirk Beyer
Claus Lewerentz
Andreas Noack


title: Hybrid Acceleration Using Real Vector Automata (Extended Abstract)

authors:
Bernard Boigelot
Frédéric Herbreteau
Sébastien Jodogne


title: Iterating Transducers in the Large (Extended Abstract)

authors:
Bernard Boigelot
Axel Legay
Pierre Wolper

abstract: Abstract. Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance. 1


title: Model Checking Multi-Agent Programs with CASP

authors:
Rafael H. Bordini
Michael Fisher
Carmen Pardavila
Willem Visser
Michael J. Wooldridge


title: Timed Control with Partial Observability

authors:
Patricia Bouyer
Deepak D'Souza
P. Madhusudan
Antoine Petit


title: HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols

authors:
Liana Bozga
Yassine Lakhnech
Michaël Périn


title: Digitizing Interval Duration Logic

authors:
Gaurav Chakravorty
Paritosh K. Pandya


title: TLQSolver: A Temporal Logic Query Checker

authors:
Marsha Chechik
Arie Gurfinkel


title: Structural Symbolic CTL Model Checking of Asynchronous Systems

authors:
Gianfranco Ciardo
Radu Siminiceanu


title: Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates

authors:
Edmund M. Clarke
Orna Grumberg
Muralidhar Talupur
Dong Wang


title: Linear Invariant Generation Using Non-linear Constraint Solving

authors:
Michael Colón
Sriram Sankaranarayanan
Henny Sipma


title: Evidence Explorer: A Tool for Exploring Model-Checking Proofs

authors:
Yifei Dong
C. R. Ramakrishnan
Scott A. Smolka


title: Monitoring Temporal Rules Combined with Time Series


title: Reasoning with Temporal Logic on Truncated Paths

authors:
Cindy Eisner
Dana Fisman
John Havlicek
Yoad Lustig
Anthony McIsaac
David Van Campenhout


title: Theorem Proving Using Lazy Proof Explication

authors:
Cormac Flanagan
Rajeev Joshi
Xinming Ou
James B. Saxe


title: An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic


title: Model Checking Conformance with Scenario-Based Specifications

authors:
Marcelo Glusman
Shmuel Katz


title: A Work-Efficient Distributed Algorithm for Reachability Analysis

authors:
Orna Grumberg
Tamir Heyman
Assaf Schuster


title: Abstraction and BDDs Complement SAT-Based BMC in DiVer

authors:
Aarti Gupta
Malay K. Ganai
Chao Wang
Zijiang Yang
Pranav Ashar


title: Thread-Modular Abstraction Refinement

authors:
Thomas A. Henzinger
Ranjit Jhala
Rupak Majumdar
Shaz Qadeer


title: Domain-Specific Optimization in Automata Learning

authors:
Hardi Hungar
Oliver Niese
Bernhard Steffen


title: Bridging the Gap between Fair Simulation and Trace Inclusion

authors:
Yonit Kesten
Nir Piterman
Amir Pnueli


title: Deductive Verification of Advanced Out-of-Order Microprocessors

authors:
Shuvendu K. Lahiri
Randal E. Bryant


title: A Symbolic Approach to Predicate Abstraction

authors:
Shuvendu K. Lahiri
Randal E. Bryant
Byron Cook


title: Interpolation and SAT-Based Model Checking


title: Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A)

authors:
Leonardo Mendonça de Moura
Harald Rueß
Maria Sorea


title: Abstraction for Branching Time Properties


title: Fast Mu-Calculus Model Checking when Tree-Width Is Bounded


title: Calculating-Confluence Compositionally

authors:
Gordon J. Pace
Frédéric Lang
Radu Mateescu


title: Certifying Optimality of State Estimation Programs

authors:
Grigore Rosu
Ram Prasad Venkatesan
Jon Whittle
Laurentiu Leustean


title: TRIM: A Tool for Triggered Message Sequence Charts

authors:
Bikram Sengupta
Rance Cleaveland


title: Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods

authors:
Sanjit A. Seshia
Randal E. Bryant


title: A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement

authors:
Sharon Shoham
Orna Grumberg


title: Dense Counter Machines and Verification Problems

authors:
Gaoyan Xie
Zhe Dang
Oscar H. Ibarra
Pierluigi San Pietro


title: Regular Model Checking for LTL(MSO)

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Marcus Nilsson
Julien d'Orso
Mayank Saksena


title: Zing: A Model Checker for Concurrent Software

authors:
Tony Andrews
Shaz Qadeer
Sriram K. Rajamani
Jakob Rehof
Yichen Xie


title: Verification of an Advanced mips-Type Out-of-Order Execution Algorithm


title: JNuke: Efficient Dynamic Analysis for Java

authors:
Cyrille Artho
Viktor Schuppan
Armin Biere
Pascal Eugster
Marcel Baur
Boris Zweimüller


title: Proving More Properties with Bounded Model Checking

authors:
Mohammad Awedh
Fabio Somenzi


title: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement

authors:
Thomas Ball
Byron Cook
Shuvendu K. Lahiri
Lintao Zhang


title: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B

authors:
Clark W. Barrett
Sergey Berezin


title: Widening Arithmetic Automata

authors:
Constantinos Bartzis
Tevfik Bultan


title: Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values

authors:
Jesse D. Bingham
Anne Condon
Alan J. Hu
Shaz Qadeer
Zhichuan Zhang


title: Abstract Regular Model Checking

authors:
Ahmed Bouajjani
Peter Habermehl
Tomás Vojnar


title: ObsSlice: A Timed Automata Slicer Based on Observers

authors:
Víctor A. Braberman
Diego Garbervetsky
Alfredo Olivero


title: Verifying omega-Regular Properties of Markov Chains

authors:
Doron Bustan
Sasha Rubin
Moshe Y. Vardi


title: Using Interface Refinement to Integrate Formal Verification into the Design Cycle

authors:
Jacob Chang
Sergey Berezin
David L. Dill


title: Formal Analysis of Java Programs in JavaFAN

authors:
Azadeh Farzan
Feng Chen
José Meseguer
Grigore Rosu


title: Image Computation in Infinite State Model Checking

authors:
Alain Finkel
Jérôme Leroux


title: Stuck-Free Conformance

authors:
Cédric Fournet
C. A. R. Hoare
Sriram K. Rajamani
Jakob Rehof


title: WSAT: A Tool for Formal Analysis of Web Services

authors:
Xiang Fu
Tevfik Bultan
Jianwen Su


title: MCK: Model Checking the Logic of Knowledge

authors:
Peter Gammie
Ron van der Meyden


title: Efficient Modeling of Embedded Memories in Bounded Model Checking

authors:
Malay K. Ganai
Aarti Gupta
Pranav Ashar


title: DPLL( T): Fast Decision Procedures

authors:
Harald Ganzinger
George Hagen
Robert Nieuwenhuis
Albert Oliveras
Cesare Tinelli


title: A Formal Reduction for Lock-Free Parallel Algorithms

authors:
Hui Gao
Wim H. Hesselink


title: Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors

authors:
Amit Goel
Randal E. Bryant


title: QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings

authors:
Ganesh Gopalakrishnan
Yue Yang
Hemanthkumar Sivaraj


title: The Mec 5 Model-Checker

authors:
Alain Griffault
Aymeric Vincent


title: Understanding Counterexamples with explain

authors:
Alex Groce
Daniel Kroening
Flavio Lerda


title: Mechanical Mathematical Methods for Microprocessor Verification


title: Verification via Structure Simulation

authors:
Neil Immerman
Alexander Moshe Rabinovich
Thomas W. Reps
Shmuel Sagiv
Greta Yorsh


title: Functional Dependency for Verification Reduction

authors:
Jie-Hong Roland Jiang
Robert K. Brayton


title: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking

authors:
HoonSang Jin
Mohammad Awedh
Fabio Somenzi


title: Abstraction-Based Satisfiability Solving of Presburger Arithmetic

authors:
Daniel Kroening
Joël Ouaknine
Sanjit A. Seshia
Ofer Strichman


title: Indexed Predicate Discovery for Unbounded System Verification

authors:
Shuvendu K. Lahiri
Randal E. Bryant


title: The UCLID Decision Procedure

authors:
Shuvendu K. Lahiri
Sanjit A. Seshia


title: Symbolic Model Checking of Non-regular Properties


title: Why Model Checking Can Improve WCET Analysis


title: SAL 2

authors:
Leonardo Mendonça de Moura
Sam Owre
Harald Rueß
John M. Rushby
Natarajan Shankar
Maria Sorea
Ashish Tiwari


title: An Experimental Evaluation of Ground Decision Procedures

authors:
Leonardo Mendonça de Moura
Harald Rueß


title: An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking


title: Rob Tristan Gerth: 1956?2003

authors:
John O'Leary
Marly Roncken


title: The HiVy Tool Set

authors:
Paula J. Pingree
Erich Mikk


title: Global Model-Checking of Infinite-State Systems

authors:
Nir Piterman
Moshe Y. Vardi


title: A Toolset for Modelling and Verification of GALS Systems

authors:
S. Ramesh
Sampada Sonalkar
Vijay D'Silva
Naveen Chandra
B. Vijayalakshmi


title: Deductive Verification of Pipelined Machines Using First-Order Quantification

authors:
Sandip Ray
Warren A. Hunt Jr.


title: Static Program Analysis via 3-Valued Logic

authors:
Thomas W. Reps
Shmuel Sagiv
Reinhard Wilhelm


title: Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings

authors:
Claus Schröter
Victor Khomenko


title: GSTE Is Partitioned Model Checking

authors:
Roberto Sebastiani
Eli Singerman
Stefano Tonetta
Moshe Y. Vardi


title: Statistical Model Checking of Black-Box Probabilistic Systems

authors:
Koushik Sen
Mahesh Viswanathan
Gul Agha


title: Range Allocation for Separation Logic

authors:
Muralidhar Talupur
Nishant Sinha
Ofer Strichman
Amir Pnueli

abstract: Separation Logic consists of a Boolean combination of predicates of the form v i ≥ v j + c where c is a constant and v i ,v j are variables of some ordered infinite type like real or integer. Any equality or inequality can be expressed in this logic. We propose a decision procedure for Separation Logic based on allocating small domains (ranges) to the formula’s variables that are sufficient for preserving satisfiability. Given a Separation Logic formula φ, our procedure constructs the inequalities graph of φ, based on φ’s predicates. This graph represents an abstraction of the formula, as there are many formulas with the same set of predicates. Our procedure then analyzes this graph and allocates a range to each variable that is adequate for all of these formulas. This approach of finding small finite ranges and enumerating them symbolically is both theoretically and empirically more efficient than methods based on case-splitting or reduction to Propositional Logic. Experimental results show that the state-space (that is, the number of assignments that need to be enumerated) allocated by our procedure is frequently exponentially smaller than previous methods.


title: PlayGame: A Platform for Diagnostic Games


title: Termination of Linear Programs


title: Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures


title: Compositional Specification and Model Checking in GSTE

authors:
Jin Yang
Carl-Johan H. Seger


title: Improved Probabilistic Models for 802.11 Protocol Verification

authors:
Amitabha Roy
K. Gopinath


title: Symbolic Compositional Verification by Learning Assumptions

authors:
Rajeev Alur
P. Madhusudan
Wonhong Nam


title: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications

authors:
Alessandro Armando
David A. Basin
Yohan Boichut
Yannick Chevalier
Luca Compagna
Jorge Cuéllar
Paul Hankes Drielsma
Pierre-Cyrille Héam
Olga Kouchnarenko
Jacopo Mantovani
Sebastian Mödersheim
David von Oheimb
Michaël Rusinowitch
Judson Santiago
Mathieu Turuani
Luca Viganò
Laurent Vigneron


title: Formal Verification of Backward Compatibility of Microcode

authors:
Tamarah Arons
Elad Elster
Limor Fix
Sela Mador-Haim
Michael Mishaeli
Jonathan Shalev
Eli Singerman
Andreas Tiemeyer
Moshe Y. Vardi
Lenore D. Zuck


title: IIV: An Invisible Invariant Verifier

authors:
Ittai Balaban
Yi Fang
Amir Pnueli
Lenore D. Zuck


title: Model Checking x86 Executables with CodeSurfer/x86 and WPDS++

authors:
Gogul Balakrishnan
Thomas W. Reps
Nicholas Kidd
Akash Lal
Junghee Lim
David Melski
Radu Gruian
Suan Hsi Yong
Chi-Hua Chen
Tim Teitelbaum


title: Abstraction for Falsification

authors:
Thomas Ball
Orna Kupferman
Greta Yorsh


title: Wolf - Bug Hunter for Concurrent Software Using Formal Methods

authors:
Sharon Barner
Ziv Glazberg
Ishai Rabinovitz


title: TVOC: A Translation Validator for Optimizing Compilers

authors:
Clark W. Barrett
Yi Fang
Benjamin Goldberg
Ying Hu
Amir Pnueli
Lenore D. Zuck


title: SMT-COMP: Satisfiability Modulo Theories Competition

authors:
Clark W. Barrett
Leonardo Mendonça de Moura
Aaron Stump


title: Verification of Tree Updates for Optimization

authors:
Michael Benedikt
Angela Bonifati
Sergio Flesca
Avinash Vyas


title: Validating a Modern Microprocessor


title: Efficient Satisfiability Modulo Theories via Delayed Theory Combination

authors:
Marco Bozzano
Roberto Bruttomesso
Alessandro Cimatti
Tommi A. Junttila
Silvio Ranise
Peter van Rossum
Roberto Sebastiani


title: Linear Ranking with Reachability

authors:
Aaron R. Bradley
Zohar Manna
Henny B. Sipma


title: Automated Assume-Guarantee Reasoning for Simulation Conformance

authors:
Sagar Chaki
Edmund M. Clarke
Nishant Sinha
Prasanna Thati


title: The ComFoRT Reasoning Framework

authors:
Sagar Chaki
James Ivers
Natasha Sharygina
Kurt C. Wallnau


title: JVer: A Java Verifier

authors:
Ajay Chander
David Espinosa
Nayeem Islam
Peter Lee
George C. Necula


title: Incremental Algorithms for Inter-procedural Analysis of Safety Properties

authors:
Christopher L. Conway
Kedar S. Namjoshi
Dennis Dams
Stephen A. Edwards


title: Cogent: Accurate Theorem Proving for Program Verification

authors:
Byron Cook
Daniel Kroening
Natasha Sharygina


title: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs

authors:
Alexandru Costan
Stephane Gaubert
Eric Goubault
Matthieu Martel
Sylvie Putot


title: Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework

authors:
Matthew B. Dwyer
John Hatcliff
Matthew Hoosier
Robby


title: Romeo: A Tool for Analyzing Time Petri Nets

authors:
Guillaume Gardey
Didier Lime
Morgan Magnin
Olivier H. Roux


title: Expand, Enlarge and Check... Made Efficient

authors:
Gilles Geeraerts
Jean-François Raskin
Laurent Van Begin


title: Abstraction Refinement for Bounded Model Checking

authors:
Anubhav Gupta
Ofer Strichman


title: Incremental and Complete Bounded Model Checking for Full PLTL

authors:
Keijo Heljanko
Tommi A. Junttila
Timo Latvala


title: F-Soft: Software Verification Platform

authors:
Franjo Ivancic
Zijiang Yang
Malay K. Ganai
Aarti Gupta
Ilya Shlyakhter
Pranav Ashar


title: Interpolant-Based Transition Relation Approximation

authors:
Ranjit Jhala
Kenneth L. McMillan


title: Program Repair as a Game

authors:
Barbara Jobstmann
Andreas Griesmayer
Roderick Bloem


title: Reasoning About Threads Communicating via Locks

authors:
Vineet Kahlon
Franjo Ivancic
Aarti Gupta


title: Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants


title: Predicate Abstraction via Symbolic Decision Procedures

authors:
Shuvendu K. Lahiri
Thomas Ball
Byron Cook


title: Extended Weighted Pushdown Systems

authors:
Akash Lal
Thomas W. Reps
Gogul Balakrishnan


title: Abstraction Refinement via Inductive Learning

authors:
Alexey Loginov
Thomas W. Reps
Shmuel Sagiv


title: Data Structure Specifications via Local Equality Axioms

authors:
Scott McPeak
George C. Necula


title: Yet Another Decision Procedure for Equality Logic

authors:
Orly Meir
Ofer Strichman


title: Compositional Analysis of Floating-Point Linear Numerical Filters


title: Randomized Algorithms for Program Analysis and Verification

authors:
George C. Necula
Sumit Gulwani


title: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic

authors:
Robert Nieuwenhuis
Albert Oliveras


title: The Orchids Intrusion Detection Tool

authors:
Julien Olivain
Jean Goubault-Larrecq


title: Concrete Model Checking with Abstract Matching and Refinement

authors:
Corina S. Pasareanu
Radek Pelánek
Willem Visser


title: TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems

authors:
Enric Pastor
Marco A. Peña
Marc Solé


title: Algorithmic Algebraic Model Checking I: Challenges from Systems Biology

authors:
Carla Piazza
Marco Antoniotti
Venkatesh Mysore
Alberto Policriti
Franz Winkler
Bud Mishra


title: Bounded Model Checking of Concurrent Programs

authors:
Ishai Rabinovitz
Orna Grumberg


title: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking

authors:
Roberto Sebastiani
Stefano Tonetta
Moshe Y. Vardi


title: On Statistical Model Checking of Stochastic Systems

authors:
Koushik Sen
Mahesh Viswanathan
Gul Agha


title: Symmetry Reduction in SAT-Based Model Checking

authors:
Daijue Tang
Sharad Malik
Aarti Gupta
C. Norris Ip


title: Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs

authors:
Eric Vecchié
Robert de Simone


title: Saturn: A SAT-Based Tool for Bug Detection

authors:
Yichen Xie
Alex Aiken


title: Action Language Verifier, Extended

authors:
Tuba Yavuz-Kahveci
Constantinos Bartzis
Tevfik Bultan


title: Probabilistic Verification for "Black-Box" Systems


title: Ymer: A Statistical Model Checker


title: Efficient Monitoring of omega-Languages

authors:
Marcelo d'Amorim
Grigore Rosu


title: Ticc: A Tool for Interface Compatibility and Composition

authors:
B. Thomas Adler
Luca de Alfaro
Leandro Dias da Silva
Marco Faella
Axel Legay
Vishwanath Raman
Pritam Roy

abstract: We present the tool Ticc ( Tool for Interface Compatibility and Composition ). In Ticc , a component interface describes both the behavior of a component, and the component’s assumptions on the environment’s behavior. Ticc can check the compatibility of such interfaces, and analyze their emergent behavior, via a symbolic implementation of game-theoretic algorithms. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Languages of Nested Trees

authors:
Rajeev Alur
Swarat Chaudhuri
P. Madhusudan


title: FAST Extended Release

authors:
Sébastien Bardin
Jérôme Leroux
Gérald Point


title: DiVinE - A Tool for Distributed Verification

authors:
Jiri Barnat
Lubos Brim
Ivana Cerná
Pavel Moravec
Petr Rockai
Pavel Simecek


title: Automatic Termination Proofs for Programs with Shape-Shifting Heaps

authors:
Josh Berdine
Byron Cook
Dino Distefano
Peter W. O'Hearn


title: Lazy Shape Analysis

authors:
Dirk Beyer
Thomas A. Henzinger
Grégory Théoduloz


title: The Power of Hybrid Acceleration

authors:
Bernard Boigelot
Frédéric Herbreteau


title: Programs with Lists Are Counter Automata

authors:
Ahmed Bouajjani
Marius Bozga
Peter Habermehl
Radu Iosif
Pierre Moro
Tomás Vojnar


title: Termination of Integer Linear Programs


title: Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study

authors:
Sebastian Burckhardt
Rajeev Alur
Milo M. K. Martin


title: Some Complexity Results for SystemVerilog Assertions

authors:
Doron Bustan
John Havlicek


title: Formal Verification of a Lazy Concurrent List-Based Set Algorithm

authors:
Robert Colvin
Lindsay Groves
Victor Luchangco
Mark Moir


title: Terminator: Beyond Safety

authors:
Byron Cook
Andreas Podelski
Andrey Rybalchenko


title: Formal Specifications on Industrial-Strength Code-From Myth to Reality


title: I Think I Voted: E-Voting vs. Democracy


title: A Fast Linear-Arithmetic Solver for DPLL(T)

authors:
Bruno Dutertre
Leonardo Mendonça de Moura


title: Don't Care Words with an Application to the Automata-Based Approach for Real Addition

authors:
Jochen Eisinger
Felix Klaedtke


title: Causal Atomicity

authors:
Azadeh Farzan
P. Madhusudan


title: Deriving Small Unsatisfiable Cores with Dominators

authors:
Roman Gershman
Maya Koifman
Ofer Strichman


title: Lookahead Widening

authors:
Denis Gopan
Thomas W. Reps


title: Repair of Boolean Programs with an Application to C

authors:
Andreas Griesmayer
Roderick Bloem
Byron Cook


title: Yasm: A Software Model-Checker for Verification and Refutation

authors:
Arie Gurfinkel
Ou Wei
Marsha Chechik


title: Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs


title: Bounded Model Checking for Weak Alternating Büchi Automata

authors:
Keijo Heljanko
Tommi A. Junttila
Misa Keinänen
Martin Lange
Timo Latvala


title: The Ideal of Verified Software


title: Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop

authors:
Himanshu Jain
Franjo Ivancic
Aarti Gupta
Ilya Shlyakhter
Chao Wang


title: Minimizing Generalized Büchi Automata

authors:
Sudeep Juvekar
Nir Piterman


title: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions

authors:
Vineet Kahlon
Aarti Gupta
Nishant Sinha


title: Check It Out: On the Efficient Formal Verification of Live Sequence Charts

authors:
Jochen Klose
Tobe Toben
Bernd Westphal
Hartmut Wittke


title: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify

authors:
Pavel Krcál
Wang Yi


title: Counterexamples with Loops for Predicate Abstraction

authors:
Daniel Kroening
Georg Weissenbacher


title: Safraless Compositional Synthesis

authors:
Orna Kupferman
Nir Piterman
Moshe Y. Vardi


title: Symmetry Reduction for Probabilistic Model Checking

authors:
Marta Z. Kwiatkowska
Gethin Norman
David Parker


title: SMT Techniques for Fast Predicate Abstraction

authors:
Shuvendu K. Lahiri
Robert Nieuwenhuis
Albert Oliveras


title: Improving Pushdown System Model Checking

authors:
Akash Lal
Thomas W. Reps


title: Abstraction for Shape Analysis with Fast and Precise Transformers

authors:
Tal Lev-Ami
Neil Immerman
Shmuel Sagiv


title: Termination Analysis with Calling Context Graphs

authors:
Panagiotis Manolios
Daron Vroon


title: Lazy Abstraction with Interpolants


title: EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation

authors:
Flavio M. de Paula
Alan J. Hu


title: The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover


title: SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation

authors:
Jan-Willem Roorda
Koen Claessen


title: Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis

authors:
Grigore Rosu
Saddek Bensalem


title: Fast and Generalized Polynomial Time Memory Consistency Verification

authors:
Amitabha Roy
Stephan Zeisset
Charles J. Fleckenstein
John C. Huang

abstract: The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor verification. We present a low complexity and fully parallelized algorithm to check program execution against the processor consistency model. In addition our algorithm is general enough to support a number of consistency models without any degradation in performance. An implementation of this algorithm is currently used in practice to verify processors in the post silicon stage for multiple architectures.


title: CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools

authors:
Koushik Sen
Gul Agha


title: Model Checking Multithreaded Programs with Asynchronous Atomic Methods

authors:
Koushik Sen
Mahesh Viswanathan


title: cascade: C Assertion Checker and Deductive Engine

authors:
Nikhil Sethi
Clark W. Barrett


title: Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation

authors:
Rachel Tzoref
Orna Grumberg


title: LEVER: A Tool for Learning Based Verification

authors:
Abhay Vardhan
Mahesh Viswanathan


title: Antichains: A New Algorithm for Checking Universality of Finite Automata

authors:
Martin De Wulf
Laurent Doyen
Thomas A. Henzinger
Jean-François Raskin


title: Parameterized Verification of Infinite-State Processes with Global Conditions

authors:
Parosh Aziz Abdulla
Giorgio Delzanno
Ahmed Rezine


title: An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games

authors:
Luca de Alfaro
Marco Faella


title: Magnifying-Lens Abstraction for Markov Decision Processes

authors:
Luca de Alfaro
Pritam Roy


title: Comparison Under Abstraction for Verifying Linearizability

authors:
Daphna Amit
Noam Rinetzky
Thomas W. Reps
Mooly Sagiv
Eran Yahav


title: Structural Abstraction of Software Verification Conditions

authors:
Domagoj Babic
Alan J. Hu


title: Leaping Loops in the Presence of Abstraction

authors:
Thomas Ball
Orna Kupferman
Mooly Sagiv


title: I/O Efficient Accepting Cycle Detection

authors:
Jiri Barnat
Lubos Brim
Pavel Simecek


title: CVC3

authors:
Clark W. Barrett
Cesare Tinelli


title: LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals

authors:
Bernd Becker
Christian Dax
Jochen Eisinger
Felix Klaedtke


title: UPPAAL-Tiga: Time for Playing Games!

authors:
Gerd Behrmann
Agnès Cougnard
Alexandre David
Emmanuel Fleury
Kim Guldstrand Larsen
Didier Lime


title: Shape Analysis for Composite Data Structures

authors:
Josh Berdine
Cristiano Calcagno
Byron Cook
Dino Distefano
Peter W. O'Hearn
Thomas Wies
Hongseok Yang


title: Algorithms for Interface Synthesis

authors:
Dirk Beyer
Thomas A. Henzinger
Vasu Singh

abstract: A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries.


title: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

authors:
Dirk Beyer
Thomas A. Henzinger
Grégory Théoduloz


title: RAT: A Tool for the Formal Analysis of Requirements

authors:
Roderick Bloem
Roberto Cavada
Ingo Pill
Marco Roveri
Andrei Tchaltsev


title: Revamping TVLA: Making Parametric Shape Analysis Competitive

authors:
Igor Bogudlov
Tal Lev-Ami
Thomas W. Reps
Mooly Sagiv


title: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures

authors:
Ahmed Bouajjani
Séverine Fratani
Shaz Qadeer


title: C32SAT: Checking C Expressions

authors:
Robert Brummayer
Armin Biere


title: A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems

authors:
Roberto Bruttomesso
Alessandro Cimatti
Anders Franzén
Alberto Griggio
Ziyad Hanna
Alexander Nadel
Amit Palti
Roberto Sebastiani


title: Verification Across Intellectual Property Boundaries

authors:
Sagar Chaki
Christian Schallhart
Helmut Veith


title: Hector: Software Model Checking with Cooperating Analysis Plugins

authors:
Nathaniel Charlton
Michael Huth


title: Parametric and Sliced Causality

authors:
Feng Chen
Grigore Rosu


title: Boolean Abstraction for Temporal Logic Satisfiability

authors:
Alessandro Cimatti
Marco Roveri
Viktor Schuppan
Stefano Tonetta


title: Local Proofs for Global Safety Properties

authors:
Ariel Cohen
Kedar S. Namjoshi


title: Automatically Proving Program Termination


title: Parallelising Symbolic State-Space Generators

authors:
Jonathan Ezekiel
Gerald Lüttgen
Gianfranco Ciardo


title: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification

authors:
Jean-Christophe Filliâtre
Claude Marché


title: Verification of Hybrid Systems


title: A Decision Procedure for Bit-Vectors and Arrays

authors:
Vijay Ganesh
David L. Dill


title: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes

authors:
Hubert Garavel
Radu Mateescu
Frédéric Lang
Wendelin Serwe


title: Low-Level Library Analysis and Summarization

authors:
Denis Gopan
Thomas W. Reps


title: An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software

authors:
Sumit Gulwani
Ashish Tiwari


title: Automated Assumption Generation for Compositional Verification

authors:
Anubhav Gupta
Kenneth L. McMillan
Zhaohui Fu


title: Array Abstractions from Proofs

authors:
Ranjit Jhala
Kenneth L. McMillan


title: Anzu: A Tool for Property Synthesis

authors:
Barbara Jobstmann
Stefan J. Galler
Martin Weiglhofer
Roderick Bloem


title: Systematic Acceleration in Regular Model Checking

authors:
Bengt Jonsson
Mayank Saksena


title: Fast and Accurate Static Data-Race Detection for Concurrent Programs

authors:
Vineet Kahlon
Yu Yang
Sriram Sankaranarayanan
Aarti Gupta


title: Three-Valued Abstraction for Continuous-Time Markov Chains

authors:
Joost-Pieter Katoen
Daniel Klink
Martin Leucker
Verena Wolf


title: Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?


title: From Liveness to Promptness

authors:
Orna Kupferman
Nir Piterman
Moshe Y. Vardi


title: A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java

authors:
Gary T. Leavens
Joseph R. Kiniry
Erik Poll


title: On Synthesizing Controllers from Bounded-Response Properties

authors:
Oded Maler
Dejan Nickovic
Amir Pnueli


title: BAT: The Bit-Level Analysis Tool

authors:
Panagiotis Manolios
Sudarshan K. Srinivasan
Daron Vroon


title: Underapproximation for Model-Checking Based on Random Cryptographic Constructions

authors:
Arie Matsliah
Ofer Strichman


title: A Tutorial on Satisfiability Modulo Theories

authors:
Leonardo Mendonça de Moura
Bruno Dutertre
Natarajan Shankar


title: Test Coverage for Continuous and Hybrid Systems

authors:
Tarik Nahhal
Thao Dang


title: The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems

authors:
Martin Ouimet
Kristina Lundqvist


title: Spade: Verification of Multithreaded Dynamic and Recursive Programs

authors:
Gaël Patin
Mihaela Sighireanu
Tayssir Touili


title: Hybrid Systems: From Verification to Falsification

authors:
Erion Plaku
Lydia E. Kavraki
Moshe Y. Vardi


title: A Mathematical Approach to RTL Verification


title: Abstraction and Counterexample-Guided Construction of omega -Automata for Model Checking of Step-Discrete Linear Hybrid Models


title: SAT-Based Compositional Verification Using Lazy Learning

authors:
Nishant Sinha
Edmund M. Clarke


title: jMoped: A Test Environment for Java Programs

authors:
Dejvuth Suwimonteerabuth
Felix Berger
Stefan Schwoon
Javier Esparza


title: Adaptive Symmetry Reduction


title: Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra

authors:
Chao Wang
Zijiang Yang
Aarti Gupta
Franjo Ivancic


title: Monotonic Abstraction for Programs with Dynamic Memory Heaps

authors:
Parosh Aziz Abdulla
Ahmed Bouajjani
Jonathan Cederberg
Frédéric Haziza
Ahmed Rezine


title: Ranking Automata and Games for Prioritized Requirements

authors:
Rajeev Alur
Aditya Kanade
Gera Weiss


title: The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis

authors:
Michael Backes
Stefan Lorenz
Matteo Maffei
Kim Pecina


title: Implied Set Closure and Its Application to Memory Consistency Verification

authors:
Surender Baswana
Shashank K. Mehta
Vishal Powar


title: Thread Quantification for Concurrent Shape Analysis

authors:
Josh Berdine
Tal Lev-Ami
Roman Manevich
G. Ramalingam
Shmuel Sagiv


title: CSIsat: Interpolation for LA+EUF

authors:
Dirk Beyer
Damien Zufferey
Rupak Majumdar


title: A Practical Approach to Word Level Model Checking of Industrial Netlists


title: Automated Assume-Guarantee Reasoning by Abstraction Refinement

authors:
Mihaela Gheorghiu Bobaru
Corina S. Pasareanu
Dimitra Giannakopoulou


title: The Barcelogic SMT Solver

authors:
Miquel Bofill
Robert Nieuwenhuis
Albert Oliveras
Enric Rodríguez-Carbonell
Albert Rubio


title: The MathSAT 4SMT Solver

authors:
Roberto Bruttomesso
Alessandro Cimatti
Anders Franzén
Alberto Griggio
Roberto Sebastiani


title: Effective Program Verification for Relaxed Memory Models

authors:
Sebastian Burckhardt
Madanlal Musuvathi


title: Local Proofs for Linear-Time Properties of Concurrent Programs

authors:
Ariel Cohen
Kedar S. Namjoshi


title: Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses

authors:
Ariel Cohen
Amir Pnueli
Lenore D. Zuck


title: Proving Conditional Termination

authors:
Byron Cook
Sumit Gulwani
Tal Lev-Ami
Andrey Rybalchenko
Mooly Sagiv


title: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols


title: Conflict-Tolerant Features

authors:
Deepak D'Souza
Madhu Gopinathan


title: Semi-external LTL Model Checking

authors:
Stefan Edelkamp
Peter Sanders
Pavel Simecek


title: Functional Verification of Power Gated Designs by Compositional Reasoning

authors:
Cindy Eisner
Amir Nahir
Karen Yorav


title: Monitoring Atomicity in Concurrent Programs

authors:
Azadeh Farzan
P. Madhusudan


title: Coping with Outside-the-Box Attacks


title: Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)


title: AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems

authors:
Ambar A. Gadkari
Anand Yeolekar
J. Suresh
S. Ramesh
Swarup Mohalik
K. C. Shashidhar


title: QMC: A Model Checker for Quantum Systems

authors:
Simon J. Gay
Rajagopal Nagarajan
Nikolaos Papanikolaou


title: Correcting a Space-Efficient Simulation Algorithm

authors:
Rob J. van Glabbeek
Bas Ploeger


title: A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis

authors:
Bhargav S. Gulavani
Sumit Gulwani


title: Constraint-Based Approach for Analysis of Hybrid Systems

authors:
Sumit Gulwani
Ashish Tiwari


title: Theorem Proving for Verification (Invited Tutorial)


title: Probabilistic CEGAR

authors:
Holger Hermanns
Björn Wachter
Lijun Zhang


title: FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement

authors:
Andreas Holzer
Christian Schallhart
Michael Tautschnig
Helmut Veith


title: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations

authors:
Himanshu Jain
Edmund M. Clarke
Orna Grumberg


title: Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems

authors:
Salil Joshi
Barbara König


title: Producing Short Counterexamples Using "Crucial Events"

authors:
Sujatha Kashyap
Vijay K. Garg


title: Application of Formal Word-Level Analysis to Constrained Random Simulation

authors:
Hyondeuk Kim
HoonSang Jin
Kavita Ravi
Petr Spacek
John Pierce
Robert P. Kurshan
Fabio Somenzi


title: Jakstab: A Static Analysis Platform for Binaries

authors:
Johannes Kinder
Helmut Veith


title: Inferring Congruence Equations Using SAT

authors:
Andy King
Harald Søndergaard


title: A Hybrid Type System for Lock-Freedom of Mobile Processes

authors:
Naoki Kobayashi
Davide Sangiorgi


title: Validating High-Level Synthesis

authors:
Sudipta Kundu
Sorin Lerner
Rajesh Gupta


title: Faster Than Uppaal?

authors:
Sebastian Kupferschmid
Martin Wehrle
Bernhard Nebel
Andreas Podelski


title: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

authors:
Akash Lal
Thomas W. Reps


title: Singularity: Designing Better Software (Invited Talk)


title: T(O)RMC: A Tool for (omega)-Regular Model Checking


title: THOR: A Tool for Reasoning about Shape and Arithmetic

authors:
Stephen Magill
Ming-Hsien Tsai
Peter Lee
Yih-Kuen Tsay


title: Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B

authors:
Laura I. Meikle
Jacques D. Fleuriot


title: Enhancing Program Verification with Lemmas

authors:
Huu Hai Nguyen
Wei-Ngan Chin


title: Discriminative Model Checking

authors:
Peter Niebert
Doron A. Peled
Amir Pnueli


title: Tutorial on Separation Logic (Invited Tutorial)


title: Linear Arithmetic with Stars

authors:
Ruzica Piskac
Viktor Kuncak


title: Computing Differential Invariants of Hybrid Systems as Fixedpoints

authors:
André Platzer
Edmund M. Clarke


title: Heap Assumptions on Demand

authors:
Andreas Podelski
Andrey Rybalchenko
Thomas Wies


title: Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings

authors:
Sarvani S. Vakkalanka
Ganesh Gopalakrishnan
Robert M. Kirby


title: An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths

authors:
Oliver Wienand
Markus Wedler
Dominik Stoffel
Wolfgang Kunz
Gert-Martin Greuel


title: Abstract Interpretation with Applications to Timing Validation

authors:
Reinhard Wilhelm
Björn Wachter


title: Scalable Shape Analysis for Systems Code

authors:
Hongseok Yang
Oukseh Lee
Josh Berdine
Cristiano Calcagno
Byron Cook
Dino Distefano
Peter W. O'Hearn


title: Models and Proofs of Protocol Security: A Progress Report

authors:
Martín Abadi
Bruno Blanchet
Hubert Comon-Lundh


title: Symbolic Counter Abstraction for Concurrent Software

authors:
Gérard Basler
Michele Mazzucchi
Thomas Wahl
Daniel Kroening


title: Priority Scheduling of Distributed Systems Based on Model Checking

authors:
Ananda Basu
Saddek Bensalem
Doron A. Peled
Joseph Sifakis


title: Explaining Counterexamples Using Causality

authors:
Ilan Beer
Shoham Ben-David
Hana Chockler
Avigail Orni
Richard J. Trefler


title: Size-Change Termination, Monotonicity Constraints and Ranking Functions


title: Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?


title: D-Finder: A Tool for Compositional Deadlock Detection and Verification

authors:
Saddek Bensalem
Marius Bozga
Thanh-Hung Nguyen
Joseph Sifakis


title: Linear Functional Fixed-points

authors:
Nikolaj S. Bjørner
Joe Hendrix


title: Better Quality in Synthesis through Quantitative Objectives

authors:
Roderick Bloem
Krishnendu Chatterjee
Thomas A. Henzinger
Barbara Jobstmann

abstract:
Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the "goodness" of an implementation. Using games with corresponding quantitative objectives, we can synthesize "optimal" implementations, which are preferred among the set of possible implementations that satisfy a given specification.

In particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.


title: HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment

authors:
Olivier Bouissou
Eric Goubault
Sylvie Putot
Karim Tekkal
Franck Védrine


title: Automatic Verification of Integer Array Programs

authors:
Marius Bozga
Peter Habermehl
Radu Iosif
Filip Konecný
Tomás Vojnar

abstract: We provide a verification technique for a class of programs working on integer arrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL [13] to specify pre- and post-conditions of programs and their parts. Effects of non-looping parts of code are computed syntactically on the level of SIL. Loop pre-conditions derived during the computation in SIL are converted into counter automata (CA). Loops are automatically translated—purely on the syntactical level—to transducers. Pre-condition CA and transducers are composed, and the composition over-approximated by flat automata with difference bound constraints, which are next converted back into SIL formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in SIL may be checked as entailment is decidable for SIL.


title: Automated Analysis of Java Methods for Confidentiality

authors:
Pavol Cerný
Rajeev Alur


title: Requirements Validation for Hybrid Systems

authors:
Alessandro Cimatti
Marco Roveri
Stefano Tonetta


title: Towards Performance Prediction of Compositional Models in Industrial GALS Designs

authors:
Nicolas Coste
Holger Hermanns
Etienne Lantreibecq
Wendelin Serwe


title: Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion

authors:
Thao Dang
David Salinas


title: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers

authors:
Isil Dillig
Thomas Dillig
Alex Aiken


title: Meta-analysis for Atomicity Violations under Nested Locking

authors:
Azadeh Farzan
P. Madhusudan
Francesco Sorrentino


title: An Antichain Algorithm for LTL Realizability

authors:
Emmanuel Filiot
Naiyong Jin
Jean-François Raskin


title: On Extending Bounded Proofs to Inductive Proofs

authors:
Oded Fuhrmann
Shlomo Hoory


title: Games through Nested Fixpoints

authors:
Thomas Gawlitza
Helmut Seidl


title: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

authors:
Yeting Ge
Leonardo Mendonça de Moura


title: The Zonotope Abstract Domain Taylor1+

authors:
Khalil Ghorbal
Eric Goubault
Sylvie Putot


title: Reachability Analysis of Hybrid Systems Using Support Functions

authors:
Colas Le Guernic
Antoine Girard


title: Software Transactional Memory on Relaxed Memory Models

authors:
Rachid Guerraoui
Thomas A. Henzinger
Vasu Singh


title: Transactional Memory: Glimmer of a Theory

authors:
Rachid Guerraoui
Michal Kapalka


title: SPEED: Symbolic Complexity Bound Analysis


title: InvGen: An Efficient Invariant Generator

authors:
Ashutosh Gupta
Andrey Rybalchenko


title: INFAMY: An Infinite-State Markov Model Checker

authors:
Ernst Moritz Hahn
Holger Hermanns
Björn Wachter
Lijun Zhang


title: Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep

authors:
Sylvain Hallé
Roger Villemaire


title: Sliding Window Abstraction for Infinite Markov Chains

authors:
Thomas A. Henzinger
Maria Mateescu
Verena Wolf


title: Homer: A Higher-Order Observational Equivalence Model checkER

authors:
David Hopkins
C.-H. Luke Ong


title: Centaur Technology Media Unit Verification

authors:
Warren A. Hunt Jr.
Sol Swords


title: Incremental Instance Generation in Local Reasoning


title: Apron: A Library of Numerical Abstract Domains for Static Analysis

authors:
Bertrand Jeannet
Antoine Miné


title: Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic

authors:
Susmit Jha
Rhishikesh Limaye
Sanjit A. Seshia


title: Quantifier Elimination via Functional Composition


title: CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs

authors:
Pallavi Joshi
Mayur Naik
Chang-Seo Park
Koushik Sen


title: Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique

authors:
Vineet Kahlon
Chao Wang
Aarti Gupta


title: Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation

authors:
Roope Kaivola
Rajnish Ghughal
Naren Narasimhan
Amber Telfer
Jesse Whittemore
Sudhindra Pandav
Anna Slobodová
Christopher Taylor
Vladimir A. Frolov
Erik Reeber
Armaghan Naik


title: Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models

authors:
Aditya Kanade
Rajeev Alur
Franjo Ivancic
S. Ramesh
Sriram Sankaranarayanan
K. C. Shashidhar


title: Mixed-Signal System Verification: A High-Speed Link Example


title: A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints

authors:
Nathan Kitchen
Andreas Kuehlmann


title: Modelling Epigenetic Information Maintenance: A Kappa Tutorial

authors:
Jean Krivine
Vincent Danos
Arndt Benecke


title: Intra-module Inference

authors:
Shuvendu K. Lahiri
Shaz Qadeer
Juan P. Galeotti
Jan W. Voung
Thomas Wies


title: Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers

authors:
Shuvendu K. Lahiri
Shaz Qadeer
Zvonimir Rakamaric


title: Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints

authors:
Peter Lammich
Markus Müller-Olm
Alexander Wenner


title: MCMAS: A Model Checker for the Verification of Multi-Agent Systems

authors:
Alessio Lomuscio
Hongyang Qu
Franco Raimondi


title: Reducing Test Inputs Using Information Partitions

authors:
Rupak Majumdar
Ru-Gang Xu


title: Generalizing DPLL to Richer Logics

authors:
Kenneth L. McMillan
Andreas Kuehlmann
Mooly Sagiv


title: On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure

abstract:
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well for typical problems arising from model-checking and program analysis (sparse inequalities, small coefficients) but are slow for other applications (denser problems, larger coefficients).

We propose a simple preprocessing phase that can be adapted to existing SMT solvers and that may be optionally triggered. Despite using floating-point computations, our method is sound and complete -- it merely affects efficiency. We implemented the method and provide benchmarks showing that this change brings a naive and slow decision procedure ("textbook simplex" with rational numbers) up to the efficiency of recent SMT solvers, over test cases arising from model-checking, and makes it definitely faster than state-of-the-art SMT solvers on dense examples.


title: TASS: Timing Analyzer of Scenario-Based Specifications

authors:
Minxue Pan
Lei Bu
Xuandong Li


title: Cardinality Abstraction for Declarative Networking Applications

authors:
Juan Antonio Navarro Pérez
Andrey Rybalchenko
Atul Singh


title: Translation Validation: From Simulink to C

authors:
Michael Ryabtsev
Ofer Strichman

abstract: Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and generates optimized C code. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Component-Based Construction of Real-Time Systems in BIP


title: VS3: SMT Solvers for Program Verification

authors:
Saurabh Srivastava
Sumit Gulwani
Jeffrey S. Foster


title: Regression Verification: Proving the Equivalence of Similar Programs


title: PAT: Towards Flexible Verification under Fairness

authors:
Jun Sun
Yang Liu
Jin Song Dong
Jun Pang


title: Reducing Context-Bounded Concurrent Reachability to Sequential Reachability

authors:
Salvatore La Torre
P. Madhusudan
Gennaro Parlato


title: Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

authors:
Sven Verdoolaege
Gerda Janssens
Maurice Bruynooghe


title: A Concurrent Portfolio Approach to SMT Solving

authors:
Christoph M. Wintersteiger
Youssef Hamadi
Leonardo Mendonça de Moura


title: Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing

authors:
Parosh Aziz Abdulla
Yu-Fang Chen
Lorenzo Clemente
Lukás Holík
Chih-Duo Hong
Richard Mayr
Tomás Vojnar


title: Abstract Analysis of Symbolic Executions

authors:
Aws Albarghouthi
Arie Gurfinkel
Ou Wei
Marsha Chechik


title: Fences in Weak Memory Models

authors:
Jade Alglave
Luc Maranget
Susmit Sarkar
Peter Sewell


title: The Static Driver Verifier Research Platform

authors:
Thomas Ball
Ella Bounimova
Vladimir Levin
Rahul Kumar
Jakob Lichtenberg


title: Policy Monitoring in First-Order Temporal Logic

authors:
David A. Basin
Felix Klaedtke
Samuel Müller


title: Robustness in the Presence of Liveness

authors:
Roderick Bloem
Krishnendu Chatterjee
Karin Greimel
Thomas A. Henzinger
Barbara Jobstmann


title: RATSY - A New Requirements Analysis Tool with Synthesis

authors:
Roderick Bloem
Alessandro Cimatti
Karin Greimel
Georg Hofferek
Robert Könighofer
Marco Roveri
Viktor Schuppan
Richard Seeber


title: LTSmin: Distributed and Symbolic Reachability

authors:
Stefan Blom
Jaco van de Pol
Michael Weber


title: libalf: The Automata Learning Framework

authors:
Benedikt Bollig
Joost-Pieter Katoen
Carsten Kern
Martin Leucker
Daniel Neider
David R. Piegdon


title: Invariant Synthesis for Programs Manipulating Lists with Unbounded Data

authors:
Ahmed Bouajjani
Cezara Dragoi
Constantin Enea
Ahmed Rezine
Mihaela Sighireanu


title: Fast Acceleration of Ultimately Periodic Relations

authors:
Marius Bozga
Radu Iosif
Filip Konecný


title: A Model Checker for AADL

authors:
Marco Bozzano
Alessandro Cimatti
Joost-Pieter Katoen
Viet Yen Nguyen
Thomas Noll
Marco Roveri
Ralf Wimmer


title: ABC: An Academic Industrial-Strength Verification Tool

authors:
Robert K. Brayton
Alan Mishchenko

abstract: ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms. A focus on the synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper introduces ABC, motivates its development, and illustrates its use in formal verification.


title: Merit: An Interpolating Model-Checker


title: Model Checking of Linearizability of Concurrent List Implementations

authors:
Pavol Cerný
Arjun Radhakrishna
Damien Zufferey
Swarat Chaudhuri
Rajeev Alur


title: Gist: A Solver for Probabilistic Games

authors:
Krishnendu Chatterjee
Thomas A. Henzinger
Barbara Jobstmann
Arjun Radhakrishna

abstract: Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.


title: Measuring and Synthesizing Systems in Probabilistic Environments

authors:
Krishnendu Chatterjee
Thomas A. Henzinger
Barbara Jobstmann
Rohit Singh


title: Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics

authors:
Satrajit Chatterjee
Michael Kishinevsky


title: Automated Assume-Guarantee Reasoning through Implicit Learning

authors:
Yu-Fang Chen
Edmund M. Clarke
Azadeh Farzan
Ming-Hsien Tsai
Yih-Kuen Tsay
Bow-Yaw Wang


title: Local Verification of Global Invariants in Concurrent Programs

authors:
Ernie Cohen
Michal Moskal
Wolfram Schulte
Stephan Tobies


title: A Dash of Fairness for Compositional Reasoning

authors:
Ariel Cohen
Kedar S. Namjoshi
Yaniv Sa'ar


title: SPLIT: A Compositional LTL Verifier


title: Verifying Low-Level Implementations of High-Level Datatypes

authors:
Christopher L. Conway
Clark W. Barrett


title: Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems


title: Symbolic Bounded Synthesis


title: A NuSMV Extension for Graded-CTL Model Checking

authors:
Alessandro Ferrante
Maurizio Memoli
Margherita Napoli
Mimmo Parente
Francesco Sorrentino


title: Bounded Underapproximations

authors:
Pierre Ganty
Rupak Majumdar
Benjamin Monmege


title: A Logical Product Approach to Zonotope Intersection

authors:
Khalil Ghorbal
Eric Goubault
Sylvie Putot

abstract: We define and study a new abstract domain which is a fine-grained combination of zonotopes with (sub-)polyhedric domains such as the interval, octagon, linear template or polyhedron domains While abstract transfer functions are still rather inexpensive and accurate even for interpreting non-linear computations, we are able to also interpret tests (i.e intersections) efficiently This fixes a known drawback of zonotopic methods, as used for reachability analysis for hybrid systems as well as for invariant generation in abstract interpretation: intersection of zonotopes are not always zonotopes, and there is not even a best zonotopic over-approximation of the intersection We describe some examples and an implementation of our method in the APRON library, and discuss some further interesting combinations of zonotopes with non-linear or non-convex domains such as quadratic templates and maxplus polyhedra.


title: Achieving Distributed Control through Model Checking

authors:
Susanne Graf
Doron A. Peled
Sophie Quinton


title: PARAM: A Model Checker for Parametric Markov Models

authors:
Ernst Moritz Hahn
Holger Hermanns
Björn Wachter
Lijun Zhang


title: Efficient Emptiness Check for Timed Büchi Automata

authors:
Frédéric Herbreteau
B. Srivathsan
Igor Walukiewicz


title: Retrofitting Legacy Code for Security


title: Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs

authors:
Vineet Kahlon
Chao Wang


title: Dynamic Cutoff Detection in Parameterized Concurrent Programs

authors:
Alexander Kaiser
Daniel Kroening
Thomas Wahl


title: Dsolve: Safety Verification via Liquid Types

authors:
Ming Kawaguchi
Patrick Maxim Rondon
Ranjit Jhala


title: Termination Analysis with Compositional Transition Invariants

authors:
Daniel Kroening
Natasha Sharygina
Aliaksei Tsitovich
Christoph M. Wintersteiger


title: Comfusy: A Tool for Complete Functional Synthesis

authors:
Viktor Kuncak
Mikaël Mayer
Ruzica Piskac
Philippe Suter


title: Contessa: Concurrency Testing Augmented with Symbolic Analysis

authors:
Sudipta Kundu
Malay K. Ganai
Chao Wang


title: Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification

authors:
Juncao Li
Fei Xie
Thomas Ball
Vladimir Levin


title: Generating Litmus Tests for Contrasting Memory Consistency Models

authors:
Sela Mador-Haim
Rajeev Alur
Milo M. K. Martin


title: Quantitative Information Flow: From Theory to Practice?


title: Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems

authors:
Federico Mari
Igor Melatti
Ivano Salvo
Enrico Tronci


title: PESSOA: A Tool for Embedded Controller Synthesis

authors:
Manuel Mazo Jr.
Anna Davitian
Paulo Tabuada


title: Lazy Annotation for Program Testing and Verification


title: Petruchio: From Dynamic Networks to Nets

authors:
Roland Meyer
Tim Strazny


title: Memory Management in Concurrent Algorithms


title: Quantifier Elimination by Lazy Model Enumeration


title: Jtlv: A Framework for Developing Verification Algorithms

authors:
Amir Pnueli
Yaniv Sa'ar
Lenore D. Zuck


title: An Abstraction-Refinement Approach to Verification of Artificial Neural Networks

authors:
Luca Pulina
Armando Tacchella


title: There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code

authors:
Thomas W. Reps
Junghee Lim
Aditya V. Thakur
Gogul Balakrishnan
Akash Lal


title: Constraint Solving for Program Verification: Theory and Practice by Example


title: Global Reachability in Bounded Phase Multi-stack Pushdown Systems


title: Learning Component Interfaces with May and Must Abstractions

authors:
Rishabh Singh
Dimitra Giannakopoulou
Corina S. Pasareanu


title: Directed Proof Generation for Machine Code

authors:
Aditya V. Thakur
Junghee Lim
Akash Lal
Amanda Burton
Evan Driscoll
Matt Elder
Tycho Andersen
Thomas W. Reps


title: Model-Checking Parameterized Concurrent Programs Using Linear Interfaces

authors:
Salvatore La Torre
P. Madhusudan
Gennaro Parlato


title: Automatically Proving Linearizability


title: Safety Verification for Probabilistic Hybrid Systems

authors:
Lijun Zhang
Zhikun She
Stefan Ratschan
Holger Hermanns
Ernst Moritz Hahn


title: On Array Theory of Bounded Elements

authors:
Min Zhou
Fei He
Bow-Yaw Wang
Ming Gu


title: Stability in Weak Memory Models

authors:
Jade Alglave
Luc Maranget


title: Verification of Certifying Computations

authors:
Eyad Alkassar
Sascha Böhme
Kurt Mehlhorn
Christine Rizkallah


title: Parameter Identification for Markov Models of Biochemical Reactions

authors:
Aleksandr Andreychenko
Linar Mikeev
David Spieler
Verena Wolf

abstract: We propose a numerical technique for parameter inference in Markov models of biological processes. Based on time-series data of a process we estimate the kinetic rate constants by maximizing the likelihood of the data. The computation of the likelihood relies on a dynamic abstraction of the discrete state space of the Markov model which successfully mitigates the problem of state space largeness. We compare two variants of our method to state-of-the-art, recently published methods and demonstrate their usefulness and efficiency on several case studies from systems biology.


title: Getting Rid of Store-Buffers in TSO Analysis

authors:
Mohamed Faouzi Atig
Ahmed Bouajjani
Gennaro Parlato


title: Malware Analysis with Tree Automata Inference

authors:
Domagoj Babic
Daniel Reynaud
Dawn Song


title: State/Event-Based LTL Model Checking under Parametric Generalized Fairness

authors:
Kyungmin Bae
José Meseguer

abstract: In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system, leading to many different variants of fairness: transition fairness, object/process fairness, actor fairness, etc. These different notions of fairness can be unified by making explicit their parametrization over the relevant entities in the system as universal quantification. We propose a state/event-based framework as well as an on-the-fly model checking algorithm to verify LTL properties under universally quantified parametric fairness assumptions, specified by generalized strong/weak fairness formulas. It enables verification of temporal properties under fairness conditions associated to dynamic entities such as new process creations. We have implemented our algorithm within the Maude system.


title: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications

authors:
Valeriy Balabanov
Jie-Hong R. Jiang


title: The BINCOA Framework for Binary Code Analysis

authors:
Sébastien Bardin
Philippe Herrmann
Jérôme Leroux
Olivier Ly
Renaud Tabary
Aymeric Vincent


title: CVC4

authors:
Clark W. Barrett
Christopher L. Conway
Morgan Deters
Liana Hadarean
Dejan Jovanovic
Tim King
Andrew Reynolds
Cesare Tinelli


title: SLAyer: Memory Safety for Systems-Level Code

authors:
Josh Berdine
Byron Cook
Samin Ishtiaq


title: CPAchecker: A Tool for Configurable Software Verification

authors:
Dirk Beyer
M. Erkan Keremoglu

abstract: Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results -- we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easy-to-extend platform, and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. CPAchecker implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on software-verification benchmarks from the literature, and compare it with other state-of-the-art model checkers. CPAchecker is an open-source toolkit and publicly available.


title: Existential Quantification as Incremental SAT

authors:
Jörg Brauer
Andy King
Jael Kriener


title: Efficient Analysis of Probabilistic Programs with an Unbounded Counter

authors:
Tomás Brázdil
Stefan Kiefer
Antonín Kucera


title: BAP: A Binary Analysis Platform

authors:
David Brumley
Ivan Jager
Thanassis Avgerinos
Edward J. Schwartz


title: Model Checking Algorithms for CTMDPs

authors:
Peter Buchholz
Ernst Moritz Hahn
Holger Hermanns
Lijun Zhang


title: Quantitative Synthesis for Concurrent Programs

authors:
Pavol Cerný
Krishnendu Chatterjee
Thomas A. Henzinger
Arjun Radhakrishna
Rohit Singh

abstract: We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized "specification free", in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures.


title: Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives

authors:
Krishnendu Chatterjee
Monika Henzinger
Manas Joglekar
Nisarg Shah

abstract: We consider Markov decision processes (MDPs) with ω-regular specifications given as parity objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. The algorithms for the computation of the almost-sure winning set for parity objectives iteratively use the solutions for the almost-sure winning set for Büchi objectives (a special case of parity objectives). Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes \(O(n \cdot \sqrt{m})\) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs often have constant out-degree, and then our symbolic algorithm takes \(O(n \cdot \sqrt{n})\) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires \(O(n \cdot \sqrt{K})\) symbolic steps, where K is the maximal number of edges of strongly connected components (scc’s) of the MDP. The win-lose algorithm requires symbolic computation of scc’s. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5·n symbolic steps, whereas our new algorithm takes 4 ·n symbolic steps.


title: Smoothing a Program Soundly and Robustly

authors:
Swarat Chaudhuri
Armando Solar-Lezama


title: A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification

authors:
Wei-Ngan Chin
Cristian Gherghina
Razvan Voicu
Quang Loc Le
Florin Craciun
Shengchao Qin


title: Kratos - A Software Model Checker for SystemC

authors:
Alessandro Cimatti
Alberto Griggio
Andrea Micheli
Iman Narasamdya
Marco Roveri


title: Efficient Scenario Verification for Hybrid Automata

authors:
Alessandro Cimatti
Sergio Mover
Stefano Tonetta


title: Temporal Property Verification as a Program Analysis Task

authors:
Byron Cook
Eric Koskinen
Moshe Y. Vardi


title: Time for Statistical Model Checking of Real-Time Systems

authors:
Alexandre David
Kim G. Larsen
Axel Legay
Marius Mikucionis
Zheng Wang


title: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs

authors:
Alastair F. Donaldson
Alexander Kaiser
Daniel Kroening
Thomas Wahl

abstract: Predicate abstraction is a key enabling technology for applying finitestate model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analyzing concurrent systems, there is little evidence of fruitful applications of predicate abstraction to shared-variable concurrent software. The goal of this paper is to close this gap. We have developed a symmetry-aware predicate abstraction strategy: it takes into account the replicated structure of C programs that consist of many threads executing the same procedure, and generates a Boolean program template whose multithreaded execution soundly overapproximates the concurrent C program. State explosion during model checking parallel instantiations of this template can now be absorbed by exploiting symmetry. We have implemented our method in the SATABS predicate abstraction framework, and demonstrate its superior performance over alternative approaches on a large range of synchronization programs.


title: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

authors:
Kamil Dudka
Petr Peringer
Tomás Vojnar


title: SpaceEx: Scalable Verification of Hybrid Systems

authors:
Goran Frehse
Colas Le Guernic
Alexandre Donzé
Scott Cotton
Rajarshi Ray
Olivier Lebeltel
Rodolfo Ripado
Antoine Girard
Thao Dang
Oded Maler


title: HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection

authors:
Vijay Ganesh
Adam Kiezun
Shay Artzi
Philip J. Guo
Pieter Hooimeijer
Michael D. Ernst


title: From Cardiac Cells to Genetic Regulatory Networks

authors:
Radu Grosu
Grégory Batt
Flavio H. Fenton
James Glimm
Colas Le Guernic
Scott A. Smolka
Ezio Bartocci


title: Threader: A Constraint-Based Verifier for Multi-threaded Programs

authors:
Ashutosh Gupta
Corneliu Popeea
Andrey Rybalchenko


title: Interactive Synthesis of Code Snippets

authors:
Tihomir Gvero
Viktor Kuncak
Ruzica Piskac


title: Forest Automata for Verification of Heap Manipulation

authors:
Peter Habermehl
Lukás Holík
Adam Rogalewicz
Jirí Simácek
Tomás Vojnar


title: Model Checking Recursive Programs with Numeric Data Types

authors:
Matthew Hague
Anthony Widjaja Lin


title: Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints

authors:
Christine Hang
Panagiotis Manolios
Vasilis Papavasileiou


title: μZ- An Efficient Engine for Fixed Points with Constraints

authors:
Krystof Hoder
Nikolaj S. Bjørner
Leonardo Mendonça de Moura


title: Using Types for Software Verification


title: HMC: Verifying Functional Programs Using Abstract Interpreters

authors:
Ranjit Jhala
Rupak Majumdar
Andrey Rybalchenko

abstract: We present Hindley-Milner-Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order functional programs to interprocedural analysis for first-order imperative programs. HMC works as follows. First, it uses the type structure of the functional program to generate a set of logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms the logical refinement constraints into a simple first-order imperative program and an invariant that holds iff the constraints are satisfiable. Finally, it uses an invariant generator for first-order imperative programs to discharge the invariant. We have implemented HMC and describe preliminary experimental results using two imperative checkers - ARMC and INTERPROC - to verify OCAML programs. By composing type-based reasoning grounded in program syntax and state-based reasoning grounded in abstract interpretation, HMC enables the fully automatic verification of programs written in modern programming languages.


title: A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations

authors:
Ajith K. John
Supratik Chakraborty


title: Bug-Assist: Assisting Fault Localization in ANSI-C Programs

authors:
Manu Jose
Rupak Majumdar


title: Synthesis of Distributed Control through Knowledge Accumulation

authors:
Gal Katz
Doron A. Peled
Sven Schewe


title: Language Equivalence for Probabilistic Automata

authors:
Stefan Kiefer
Andrzej S. Murawski
Joël Ouaknine
Björn Wachter
James Worrell


title: Formalization and Automated Verification of RESTful Behavior

authors:
Uri Klein
Kedar S. Namjoshi


title: Linear Completeness Thresholds for Bounded Model Checking

authors:
Daniel Kroening
Joël Ouaknine
Ofer Strichman
Thomas Wahl
James Worrell


title: Interpolation-Based Software Verification with Wolverine

authors:
Daniel Kroening
Georg Weissenbacher


title: Synthesizing Biological Theories

authors:
Hillel Kugler
Cory Plock
Andy Roberts


title: PRISM 4.0: Verification of Probabilistic Real-Time Systems

authors:
Marta Z. Kwiatkowska
Gethin Norman
David Parker


title: SMT-Based Modular Analysis of Sequential Systems Code


title: Program Analysis for Overlaid Data Structures

authors:
Oukseh Lee
Hongseok Yang
Rasmus Petersen


title: KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs

authors:
Guodong Li
Indradeep Ghosh
Sreeranga P. Rajan


title: Fully Symbolic Model Checking for Timed Automata

authors:
Georges Morbé
Florian Pigorsch
Christoph Scholl


title: Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus

authors:
Christian Müller
Wolfgang J. Paul


title: Synthia: Verification and Synthesis for Timed Automata

authors:
Hans-Jörg Peter
Rüdiger Ehlers
Robert Mattmüller


title: FixBag: A Fixpoint Calculator for Quantified Bag Constraints

authors:
Tuan-Hung Pham
Minh-Thai Trinh
Anh-Hoang Truong
Wei-Ngan Chin


title: Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial)


title: Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP

authors:
Vasumathi Raman
Hadas Kress-Gazit


title: Practical, Low-Effort Equivalence Verification of Real Code

authors:
David A. Ramos
Dawson R. Engler


title: Relational Abstractions for Continuous and Hybrid Systems

authors:
Sriram Sankaranarayanan
Ashish Tiwari


title: Simplifying Loop Invariant Generation Using Splitter Predicates

authors:
Rahul Sharma
Isil Dillig
Thomas Dillig
Alex Aiken


title: Using Coverage to Deploy Formal Verification in a Simulation World

authors:
Vigyan Singhal
Prashant Aggarwal

abstract: Formal verification technology has today advanced to the stage that it can complement or replace simulation effort for selected hardware designs. Yet the completion of a formal verification effort is rarely a requirement for hardware tapeout. Simulation remains the primary verification methodology, and means of deciding when verification is complete. In this paper we discuss how formal verification can be deployed using simulation-based coverage in a simulation-based verification schedule.


title: Monitorability of Stochastic Dynamical Systems

authors:
A. Prasad Sistla
Milos Zefran
Yao Feng


title: Equality-Based Translation Validator for LLVM

authors:
Michael Stepp
Ross Tate
Sorin Lerner


title: Resource Aware ML

authors:
Jan Hoffmann
Klaus Aehlig
Martin Hofmann


title: Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification

authors:
Aws Albarghouthi
Yi Li
Arie Gurfinkel
Marsha Chechik


title: SAFARI: SMT-Based Abstraction for Arrays with Interpolants

authors:
Francesco Alberti
Roberto Bruttomesso
Silvio Ghilardi
Silvio Ranise
Natasha Sharygina


title: Joogie: Infeasible Code Detection for Java

authors:
Stephan Arlt
Martin Schäf


title: Recent Developments in FDR

authors:
Philip J. Armstrong
Michael Goldsmith
Gavin Lowe
Joël Ouaknine
Hristina Palikareva
A. W. Roscoe
James Worrell


title: Detecting Fair Non-termination in Multithreaded Programs

authors:
Mohamed Faouzi Atig
Ahmed Bouajjani
Michael Emmi
Akash Lal


title: Bma: Visual Tool for Modeling and Analyzing Biological Networks

authors:
David Benqué
Sam Bourton
Caitlin Cockerton
Byron Cook
Jasmin Fisher
Samin Ishtiaq
Nir Piterman
Alex S. Taylor
Moshe Y. Vardi


title: Diagnosing Abstraction Failure for Separation Logic-Based Analyses

authors:
Josh Berdine
Arlen Cox
Samin Ishtiaq
Christoph M. Wintersteiger


title: Synthesizing Programs with Constraint Solvers

authors:
Rastislav Bodík
Emina Torlak


title: A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx

authors:
Sergiy Bogomolov
Goran Frehse
Radu Grosu
Hamed Ladan
Andreas Podelski
Martin Wehrle


title: Acacia+, a Tool for LTL Synthesis

authors:
Aaron Bohy
Véronique Bruyère
Emmanuel Filiot
Naiyong Jin
Jean-François Raskin


title: IC3 and beyond: Incremental, Inductive Verification


title: Efficient Controller Synthesis for Consumption Games with Multiple Resource Types

authors:
Tomás Brázdil
Krishnendu Chatterjee
Antonín Kucera
Petr Novotný


title: Automated Termination Proofs for Java Programs with Cyclic Data

authors:
Marc Brockschmidt
Richard Musiol
Carsten Otto
Jürgen Giesl


title: Euler: A System for Numerical Optimization of Programs

authors:
Swarat Chaudhuri
Armando Solar-Lezama


title: Learning Boolean Functions Incrementally

authors:
Yu-Fang Chen
Bow-Yaw Wang


title: MGSyn: Automatic Synthesis for Industrial Automation

authors:
Chih-Hong Cheng
Michael Geisinger
Harald Ruess
Christian Buckl
Alois C. Knoll


title: A Complete Method for Symmetry Reduction in Safety Verification

authors:
Duc-Hiep Chu
Joxan Jaffar


title: Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System

authors:
Alessandro Cimatti
Raffaele Corvino
Armando Lazzaro
Iman Narasamdya
Tiziana Rizzo
Marco Roveri
Angela Sanseviero
Andrei Tchaltsev


title: Software Model Checking via IC3

authors:
Alessandro Cimatti
Alberto Griggio


title: Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper

authors:
Sylvain Conchon
Amit Goel
Sava Krstic
Alain Mebsout
Fatiha Zaïdi


title: Model Checking Cell Biology


title: Minimum Satisfying Assignments for SMT

authors:
Isil Dillig
Thomas Dillig
Kenneth L. McMillan
Alex Aiken


title: OpenNWA: A Nested-Word Automaton Library

authors:
Evan Driscoll
Aditya V. Thakur
Thomas W. Reps


title: ACTL ∩ LTL Synthesis


title: Proving Termination of Probabilistic Programs Using Patterns

authors:
Javier Esparza
Andreas Gaiser
Stefan Kiefer

abstract: Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one ("almost-sure termination"), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a "terminating pattern", which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.


title: Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement

authors:
Matthew Fredrikson
Richard Joiner
Somesh Jha
Thomas W. Reps
Phillip A. Porras
Hassen Saïdi
Vinod Yegneswaran


title: Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits

authors:
Calin C. Guet
Ashutosh Gupta
Thomas A. Henzinger
Maria Mateescu
Ali Sezgin


title: On Decidability of Prebisimulation for Timed Automata

authors:
Shibashis Guha
Chinmay Narayan
S. Arun-Kumar


title: Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters

authors:
Matthew Hague
Anthony Widjaja Lin


title: When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way

authors:
Cheng-Shen Han
Jie-Hong Roland Jiang


title: Secure Programming via Visibly Pushdown Safety Games

authors:
William R. Harris
Somesh Jha
Thomas W. Reps


title: Incremental, Inductive CTL Model Checking

authors:
Zyad Hassan
Aaron R. Bradley
Fabio Somenzi


title: Exercises in Nonstandard Static Analysis of Hybrid Systems

authors:
Ichiro Hasuo
Kohei Suenaga


title: Hector: An Equivalence Checker for a Higher-Order Fragment of ML

authors:
David Hopkins
Andrzej S. Murawski
C.-H. Luke Ong


title: TRACER: A Symbolic Execution Tool for Verification

authors:
Joxan Jaffar
Vijayaraghavan Murali
Jorge A. Navas
Andrew E. Santosa


title: Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking

authors:
Cyrille Jégourel
Axel Legay
Sean Sedwards

abstract:
Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating probabilities from multiple executions of a system and by giving results within confidence bounds. Rare properties are often important but pose a particular challenge for simulation-based approaches, hence a key objective for statistical model checking (SMC) is to reduce the number and length of simulations necessary to produce a result with a given level of confidence. Importance sampling can achieves this, however to maintain the advantages of SMC it is necessary to find good importance sampling distributions without considering the entire state space.

Here we present a simple algorithm that uses the notion of cross-entropy to find an optimal importance sampling distribution. In contrast to previous work, our algorithm uses a naturally defined low dimensional vector of parameters to specify this distribution and thus avoids the intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency. We demonstrate the efficacy of our methodology by applying it to models from reliability engineering and biochemistry.


title: Lock Removal for Concurrent Trace Programs

authors:
Vineet Kahlon
Chao Wang


title: APEX: An Analyzer for Open Probabilistic Programs

authors:
Stefan Kiefer
Andrzej S. Murawski
Joël Ouaknine
Björn Wachter
James Worrell


title: Assume-Guarantee Abstraction Refinement for Probabilistic Systems

authors:
Anvesh Komuravelli
Corina S. Pasareanu
Edmund M. Clarke

abstract: We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probabilistic Transition Systems (LPTSes). We first characterize counterexamples to strong simulation as stochastic trees and show that simpler structures are insufficient. Then, we use these trees in an abstraction refinement algorithm that computes the assumptions for assume-guarantee reasoning as conservative LPTS abstractions of some of the system components. The abstractions are automatically refined based on tree counterexamples obtained from failed simulation checks with the remaining components. We have implemented the algorithms for counterexample generation and assume-guarantee abstraction refinement and report encouraging results.


title: Automatic Quantification of Cache Side-Channels

authors:
Boris Köpf
Laurent Mauborgne
Martín Ochoa


title: Deterministic Automata for the (F, G)-Fragment of LTL

authors:
Jan Kretínský
Javier Esparza

abstract: When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the ( F , G )-fragment of LTL into deterministic ω-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.


title: SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs

authors:
Shuvendu K. Lahiri
Chris Hawblitzel
Ming Kawaguchi
Henrique Rebêlo


title: A Solver for Reachability Modulo Theories

authors:
Akash Lal
Shaz Qadeer
Shuvendu K. Lahiri


title: Termination Analysis with Algorithmic Learning

authors:
Wonchan Lee
Bow-Yaw Wang
Kwangkeun Yi


title: An Axiomatic Memory Model for POWER Multiprocessors

authors:
Sela Mador-Haim
Luc Maranget
Susmit Sarkar
Kayvan Memarian
Jade Alglave
Scott Owens
Rajeev Alur
Milo M. K. Martin
Peter Sewell
Derek Williams


title: Approximately Bisimilar Symbolic Models for Digital Control Systems

authors:
Rupak Majumdar
Majid Zamani


title: From C to Infinity and Back: Unbounded Auto-active Verification with VCC


title: Formal Verification of Genetic Circuits


title: nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces

authors:
Flavio M. de Paula
Alan J. Hu
Amir Nahir


title: Leveraging Interpolant Strength in Model Checking

authors:
Simone Fulvio Rollini
Ondrej Sery
Natasha Sharygina


title: CSolve: Verifying C with Liquid Types

authors:
Patrick Maxim Rondon
Alexander Bakst
Ming Kawaguchi
Ranjit Jhala


title: How to Prove Algorithms Linearisable

authors:
Gerhard Schellhorn
Heike Wehrheim
John Derrick


title: passert: A Tool for Debugging Parallel Programs

authors:
Daniel Schwartz-Narbonne
Feng Liu
David I. August
Sharad Malik


title: Interpolants as Classifiers

authors:
Rahul Sharma
Aditya V. Nori
Alex Aiken


title: Synthesizing Number Transformations from Input-Output Examples

authors:
Rishabh Singh
Sumit Gulwani


title: SPT: Storyboard Programming Tool

authors:
Rishabh Singh
Armando Solar-Lezama

abstract: We present Spt, a tool that helps programmers write low-level data-structure manipulations by combining various forms of insights such as abstract and concrete input-output examples as well as implementation skeletons. When programmers write such manipulations, they typically have a clear high-level intuition about how the manipulation should work, but implementing efficient low-level pointer manipulating code is error-prone. Our tool aims to bridge the gap between the intuition and the corresponding implementation by automatically synthesizing the implementation. The tool frames the synthesis problem as a generalization of an abstract-interpretation based shape analysis, and represents the problem as a set of constraints which are solved efficiently by the Sketch solver. We report the successful evaluation of our tool on synthesizing several linked list and binary search tree manipulations.


title: Alternate and Learn: Finding Witnesses without Looking All over

authors:
Nishant Sinha
Nimit Singhania
Satish Chandra
Manu Sridharan


title: A Model Checker for Hierarchical Probabilistic Real-Time Systems

authors:
Songzheng Song
Jun Sun
Yang Liu
Jin Song Dong


title: A Method for Symbolic Computation of Abstract Operations

authors:
Aditya V. Thakur
Thomas W. Reps


title: Synthesis and Some of Its Challenges


title: HybridSAL Relational Abstracter


title: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants


title: Timed Relational Abstractions for Sampled Data Control Systems

authors:
Aditya Zutshi
Sriram Sankaranarayanan
Ashish Tiwari


title: Learning Universally Quantified Invariants of Linear Data Structures

authors:
Pranav Garg
Christof Löding
P. Madhusudan
Daniel Neider

abstract: We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.


title: Relative Equivalence in the Presence of Ambiguity

authors:
Oshri Adler
Cindy Eisner
Tatyana Veksler


title: Recursive Program Synthesis

authors:
Aws Albarghouthi
Sumit Gulwani
Zachary Kincaid


title: Beautiful Interpolants

authors:
Aws Albarghouthi
Kenneth L. McMillan


title: Partial Orders for Efficient Bounded Model Checking of Concurrent Software

authors:
Jade Alglave
Daniel Kroening
Michael Tautschnig


title: Automatic Generation of Quality Specifications

authors:
Shaull Almagor
Guy Avni
Orna Kupferman


title: PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems

authors:
Étienne André
Yang Liu
Jun Sun
Jin Song Dong
Shang-Wei Lin


title: SVA and PSL Local Variables - A Practical Approach

authors:
Roy Armoni
Dana Fisman
Naiyong Jin


title: DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs

authors:
Jiri Barnat
Lubos Brim
Vojtech Havel
Jan Havlícek
Jan Kriho
Milan Lenco
Petr Rockai
Vladimír Still
Jirí Weiser


title: Solving Existentially Quantified Horn Clauses

authors:
Tewodros A. Beyene
Corneliu Popeea
Andrey Rybalchenko


title: Distributed Explicit State Model Checking of Deadlock Freedom

authors:
Brad D. Bingham
Jesse D. Bingham
John Erickson
Mark R. Greenstreet


title: QUAIL: A Quantitative Security Analyzer for Imperative Code

authors:
Fabrizio Biondi
Axel Legay
Louis-Marie Traonouez
Andrzej Wasowski


title: Formal Verification of Hardware Synthesis

authors:
Thomas Braibant
Adam Chlipala

abstract: We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently typed deep embedding in Coq. The target language of the compiler corresponds to a synthesisable subset of Verilog or VHDL. A key aspect of our approach is that input programs to the compiler can be defined and proved correct inside Coq. Then, we use extraction and a Verilog back-end (written in OCaml) to get a certified version of a hardware design.


title: PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games


title: Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking

authors:
Lubos Brim
Milan Ceska
Sven Drazan
David Safránek


title: Better Termination Proving through Cooperation

authors:
Marc Brockschmidt
Byron Cook
Carsten Fuhs


title: Efficient Synthesis for Concurrency by Semantics-Preserving Transformations

authors:
Pavol Cerný
Thomas A. Henzinger
Arjun Radhakrishna
Leonid Ryzhyk
Thorsten Tarrach


title: Combining Relational Learning with SMT Solvers Using CEGAR

authors:
Arun Tejasvi Chaganty
Akash Lal
Aditya V. Nori
Sriram K. Rajamani


title: Probabilistic Program Analysis with Martingales

authors:
Aleksandar Chakarov
Sriram Sankaranarayanan


title: A Scalable and Nearly Uniform Generator of SAT Witnesses

authors:
Supratik Chakraborty
Kuldeep S. Meel
Moshe Y. Vardi

abstract: Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed random testing, where a model of the system is simulated with a set of random test stimuli that are uniformly or near-uniformly distributed over the space of all stimuli satisfying a given set of constraints. Uniform or near-uniform generation of solutions for large constraint sets is therefore a problem of theoretical and practical interest. For Boolean constraints, prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We offer here a new approach with theoretical performance guarantees and demonstrate its practical utility on large constraint sets. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

authors:
Krishnendu Chatterjee
Andreas Gaiser
Jan Kretínský

abstract: The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.


title: Faster Algorithms for Markov Decision Processes with Low Treewidth

authors:
Krishnendu Chatterjee
Jakub Lacki

abstract: We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n ·k2.38 ·2k) and O(m ·logn ·k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known $O(n\cdot k \cdot \sqrt{n\cdot k})$ bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.


title: Flow*: An Analyzer for Non-linear Hybrid Systems

authors:
Xin Chen
Erika Ábrahám
Sriram Sankaranarayanan


title: JBernstein: A Validity Checker for Generalized Polynomial Constraints

authors:
Chih-Hong Cheng
Harald Ruess
Natarajan Shankar


title: Lengths May Break Privacy - Or How to Check for Equivalences with Length

authors:
Vincent Cheval
Véronique Cortier
Antoine Plet


title: A Tool for Estimating Information Leakage

authors:
Tom Chothia
Yusuke Kawamoto
Chris Novakovic


title: Model-Checking Signal Transduction Networks through Decreasing Reachability Sets

authors:
Koen Claessen
Jasmin Fisher
Samin Ishtiaq
Nir Piterman
Qinsi Wang


title: Towards Distributed Software Model-Checking Using Decision Diagrams

authors:
Maximilien Colange
Souheib Baarir
Fabrice Kordon
Yann Thierry-Mieg


title: Equivalence of Extended Symbolic Finite Transducers

authors:
Loris D'Antoni
Margus Veanes


title: Generating Non-linear Interpolants by Semidefinite Programming

authors:
Liyun Dai
Bican Xia
Naijun Zhan

abstract: Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model checking, CEGAR, SMT, etc., in which the hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In this paper, we provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples.


title: Explain: A Tool for Performing Abductive Inference

authors:
Isil Dillig
Thomas Dillig


title: Efficient Robust Monitoring for STL

authors:
Alexandre Donzé
Thomas Ferrère
Oded Maler


title: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates

authors:
Cezara Dragoi
Ashutosh Gupta
Thomas A. Henzinger


title: Parameterized Verification of Asynchronous Shared-Memory Systems

authors:
Javier Esparza
Pierre Ganty
Rupak Majumdar


title: A Fully Verified Executable LTL Model Checker

authors:
Javier Esparza
Peter Lammich
René Neumann
Tobias Nipkow
Alexander Schimpf
Jan-Georg Smaus


title: Program Repair without Regret

authors:
Christian von Essen
Barbara Jobstmann


title: Duet: Static Analysis for Unbounded Parallelism

authors:
Azadeh Farzan
Zachary Kincaid


title: Proving Termination Starting from the End

authors:
Pierre Ganty
Samir Genaim

abstract: We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termination proof. While the proof keeps changing, the program remains the same. Our technique goes a step further. We show how to use the current partial proof to partition the transition relation into those behaviors known to be terminating from the current proof, and those whose status (terminating or not) is not known yet. This partition enables a new and unexplored dimension of incremental reasoning on the program side. In addition, we show that our approach naturally applies to conditional termination which searches for a precondition ensuring termination. We further report on a prototype implementation that advances the state-of-the-art on the grounds of termination and conditional termination.


title: SeLoger: A Tool for Graph-Based Reasoning in Separation Logic

authors:
Christoph Haase
Samin Ishtiaq
Joël Ouaknine
Matthew J. Parkinson


title: Validating Library Usage Interactively

authors:
William R. Harris
Guoliang Jin
Shan Lu
Somesh Jha


title: Software Model Checking for People Who Love Automata

authors:
Matthias Heizmann
Jochen Hoenicke
Andreas Podelski