The Human in Formal Methods (abstract)

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (abstract)

Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (abstract)

Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (abstract)

On the Nature of Symbolic Execution (abstract)

GR(1)*: GR(1) Specifications Extended with Existential Guarantees (abstract)

Counterexample-Driven Synthesis for Probabilistic Program Sketches (abstract)

Synthesis of Railway Signaling Layout from Local Capacity Specifications (abstract)

Pegasus: A Framework for Sound Continuous Invariant Generation (abstract)

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems (abstract)

Verifying Correctness of Persistent Concurrent Data Structures (abstract)

Compositional Verication of Concurrent Systems by Combining Bisimulations (abstract)

Alloy*: a general-purpose higher-order relational constraint solver (abstract)

Towards a Model-Checker for Circus (abstract)

Circus2CSP: A Tool for Model-Checking Circus Using FDR (abstract)

Formal Methods for Security Functionality and for Secure Functionality (abstract)

How Hard is Finding Shortest Counter-Example Lassos in Model Checking? (abstract)

From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (abstract)

Generic Partition Refinement and Weighted Tree Automata (abstract)

Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (abstract)

Abstract Execution (abstract)

Static Analysis for Detecting High-Level Races in RTOS Kernels (abstract)

Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (abstract)

An Axiomatic Approach to Liveness for Differential Equations (abstract)

Successes in Deployed Verified Software (and Insights on Key Social Factors) (abstract)

Local Consistency Check in Synchronous Dataflow Models (abstract)

Quantitative Verification of Numerical Stability for Kalman Filters (abstract)

Concolic Testing Heap-Manipulating Programs (abstract)

Gray-Box Monitoring of Hyperproperties (abstract)

Formal Semantics Extraction from Natural Language Specifications for ARM (abstract)

GOSPEL - Providing OCaml with a Formal Specification Language (abstract)

Unification in Matching Logic (abstract)

Embedding High-Level Formal Specifications into Applications (abstract)

Value-Dependent Information-Flow Security on Weak Memory Models (abstract)

Reasoning Formally about Database Queries and Updates (abstract)

Abstraction and Subsumption in Modular Verification of C Programs (abstract)

Unifying separation logic and region logic to allow interoperability (abstract)

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (abstract)

APML: An Architecture Proof Modelling Language (abstract)

Learning Deterministic Variable Automata over Infinite Alphabets (abstract)

L*-Based Learning of Markov Decision Processes (abstract)

Star-Based Reachability Analysis of Deep Neural Networks (abstract)

Conditions of contracts for separating responsibilities in heterogeneous systems (abstract)

SOA and the Button Problem (abstract)

Controlling Large Boolean Networks with Temporary and Permanent Perturbations (abstract)