Linked e-resources
Details
Table of Contents
A Trusted Mechanised Specification of JavaScript: One Year On
Model Checking and Refinements
On Automation of CTL* Verification for Infinite-State Systems
Algorithms for Model Checking HyperLTL and HyperCTL
Fairness Modulo Theory: A New Approach to LTL Software Model Checking
Model Checking Parameterized Asynchronous Shared-Memory Systems
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Skipping Refinement
Quantitative Reasoning
Percentile Queries in Multi-dimensional Markov Decision Processes
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes
Symbolic Polytopes for Quantitative Interpolation and Verification
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks
PROPhESY: A PRObabilistic ParamEter SYnthesis Tool
Software Analysis
Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints
Automata-Based Model Counting for String Constraints
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case
Tree Buffers
Learning Commutativity
Specifications
Angelic Verification: Precise Verification Modulo Unknowns
The SeaHorn Verification Framework
Automatic Rootcausing for Program Equivalence Failures in Binaries
Fine-Grained Caching of Verification Results
Predicting a Correct Program in Programming by Example
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
Lightning Talks
ADAM: Causality-Based Synthesis of Distributed Systems
Alchemist: Learning Guarded Affine Functions
OptiMathSAT: A Tool for Optimization Modulo Theories
Systematic Asynchrony Bug Exploration for Android Apps
Norn: An SMT Solver for String Constraints
PVSio-web 2.0: Joining PVS to HCI
The Hanoi Omega-Automata Format
The Open-Source LearnLib: A Framework for Active Automata Learning
BBS: A Phase-Bounded Model Checker for Asynchronous Programs
Time-Aware Abstractions in HybridSal
A Type-Directed Approach to Program Repair
Formal Design and Safety Analysis of AIR6110 Wheel Brake System
Meeting a Powertrain Verification Challenge
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
Empirical Software Metrics for Benchmarking of Verification Tools
Interpolation, IC3/PDR, and Invariants Property-Directed Inference of Universal Invariants or Proving Their Absence
Efficient Anytime Techniques for Model-Based Safety Analysis
Boosting k-induction with Continuously-Refined Invariants
Fast Interpolating BMC
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation.
Model Checking and Refinements
On Automation of CTL* Verification for Infinite-State Systems
Algorithms for Model Checking HyperLTL and HyperCTL
Fairness Modulo Theory: A New Approach to LTL Software Model Checking
Model Checking Parameterized Asynchronous Shared-Memory Systems
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Skipping Refinement
Quantitative Reasoning
Percentile Queries in Multi-dimensional Markov Decision Processes
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes
Symbolic Polytopes for Quantitative Interpolation and Verification
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks
PROPhESY: A PRObabilistic ParamEter SYnthesis Tool
Software Analysis
Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints
Automata-Based Model Counting for String Constraints
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case
Tree Buffers
Learning Commutativity
Specifications
Angelic Verification: Precise Verification Modulo Unknowns
The SeaHorn Verification Framework
Automatic Rootcausing for Program Equivalence Failures in Binaries
Fine-Grained Caching of Verification Results
Predicting a Correct Program in Programming by Example
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
Lightning Talks
ADAM: Causality-Based Synthesis of Distributed Systems
Alchemist: Learning Guarded Affine Functions
OptiMathSAT: A Tool for Optimization Modulo Theories
Systematic Asynchrony Bug Exploration for Android Apps
Norn: An SMT Solver for String Constraints
PVSio-web 2.0: Joining PVS to HCI
The Hanoi Omega-Automata Format
The Open-Source LearnLib: A Framework for Active Automata Learning
BBS: A Phase-Bounded Model Checker for Asynchronous Programs
Time-Aware Abstractions in HybridSal
A Type-Directed Approach to Program Repair
Formal Design and Safety Analysis of AIR6110 Wheel Brake System
Meeting a Powertrain Verification Challenge
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
Empirical Software Metrics for Benchmarking of Verification Tools
Interpolation, IC3/PDR, and Invariants Property-Directed Inference of Universal Invariants or Proving Their Absence
Efficient Anytime Techniques for Model-Based Safety Analysis
Boosting k-induction with Continuously-Refined Invariants
Fast Interpolating BMC
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation.