Resource Analysis: From Sequential to Concurrent and Distributed Programs (abstract)

Direct formal verification of liveness properties in continuous and hybrid dynamical systems (abstract)

Counterexamples for Expected Rewards (abstract)

Probabilistic Bisimulation for Realistic Schedulers (abstract)

Abstraction of Elementary Hybrid Systems by Variable Transformation (abstract)

Certified Reasoning with Infinity (abstract)

Detection of Design Flaws in the Android Permission Protocol through Bounded Verification (abstract)

Privacy by design in practice: reasoning about privacy properties of biometric system architectures (abstract)

Verifying Parameterized Timed Security Protocols (abstract)

Using Real-Time Maude to Model Check Energy Consumption Behavior (abstract)

Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (abstract)

Parameter Synthesis through Temporal Logic Specifications (abstract)

Verifying the Safety of a Flight-Critical System (abstract)

A Specification Language for Static and Runtime Verification of Data and Control Properties (abstract)

Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes (abstract)

What Should Math Have to do with Building Complex Distributed Systems? (abstract)

AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned (abstract)

Semantics-Preserving Simplification of Real-World Firewall Rule Sets (abstract)

Automated Verification of RPC Stub Code (abstract)

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (abstract)

A Fully Verified Container Library (abstract)

Using Simulink Design Verifier for Automatic Generation of Requirements-based Tests (abstract)

Practices for Formal Models as Documents: Evolution of VDM Application to ``Mobile FeliCa" IC Chip Firmware (abstract)

Formalizing the Concept Phase of Product Development at Philips Healthcare (abstract)

Analyzing the Restart Behavior of Industrial Control Applications (abstract)

Software Development and Authentication for Arms Control Information Barriers (abstract)

Verifying Opacity of a Transactional Mutex Lock (abstract)

A framework for correctness criteria on weak memory models (abstract)

Property-Driven Fence Insertion using Reorder Bounded Model Checking (abstract)

Autofunk: an inference-based formal model generation framework for production systems. (abstract)

Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking (abstract)

Formal Virtual Modelling and Data Verification for Supervision Systems (abstract)

Case Study: Static Security Analysis of the Android Goldfish Kernel (abstract)

The key role of formal methods to overcome the interoperability challenge. (abstract)

Certificates for Parameterized Model Checking (abstract)

Proving Safety with Trace Automata and Bounded Model Checking (abstract)

QPMC: A Model Checker for Quantum Programs and Protocols (abstract)

Automated Circular Assume-Guarantee Reasoning (abstract)

Model-Based Problem Solving for University Timetable Validation and Improvement (abstract)

Narrowing operators on template abstract domains (abstract)

Static Differential Program Analysis for Software-Defined Networks (abstract)

Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking (abstract)

The Semantics of Cardinality-based Feature Models via Formal Languages (abstract)

Towards Formal Verification of Orchestration Computations Using the K Framework (abstract)

Typed First-Order Logic (abstract)