A Logical Approach to Systems Engineering Artifacts: Semantic Relationships and Dependencies beyond Traceability - From Requirements to Functional and Architectural View ( abstract )

An algebra of synchronous atomic steps ( abstract )

Explaining Relaxed Memory Models with Program Transformations ( abstract )

Error Invariants for Concurrent Traces ( abstract )

A Generic Logic for Proving Linearizability ( abstract )

Dealing with Incompleteness in Automata-based Model Checking ( abstract )

A Model Checking Approach to Discrete Bifurcation Analysis ( abstract )

Regression Verification for unbalanced recursive functions ( abstract )

GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking ( abstract )

Compositional Parameter Synthesis ( abstract )

A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems ( abstract )

Approximate Bisimulation and Discretization of Hybrid CSP ( abstract )

Towards Concolic Testing for Hybrid Systems ( abstract )

From Electrical Switched Networks to Hybrid Automata ( abstract )

State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI ( abstract )

Tighter Reachability Criteria for Deadlock-Freedom Analysis ( abstract )

Danger Invariants ( abstract )

Automated Mutual Explicit Induction Proof in Separation Logic ( abstract )

Recovering high-level conditions from binary programs ( abstract )

Formal Verification of Multi-Paxos for Distributed Consensus ( abstract )

Moving Fast with Program Verification Technology ( abstract )

Modal Kleene Algebra Applied to Program Correctness ( abstract )

Mechanised Verification Patterns for Dafny ( abstract )

Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations ( abstract )

Sound and Complete Mutation-Based Program Repair ( abstract )

Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems ( abstract )

Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations ( abstract )

RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions ( abstract )

Model-Based Design of an Energy-System Embedded Controller using Taste ( abstract )

Learning Moore Machines from Input-Output Traces ( abstract )

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions ( abstract )

Exploring Model Quality for ACAS X ( abstract )

Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation ( abstract )

Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers ( abstract )

Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller ( abstract )

Industrial-strength Model-based Testing of Safety-critical Systems ( abstract )

Battery-Aware Scheduling in Low Orbit: The GomX-3 Case ( abstract )

Discounted Duration Calculus ( abstract )

Validated Simulation-Based Verification of Delayed Differential Dynamics ( abstract )

Local Planning of Multiparty Interactions with Bounded Horizons ( abstract )

Refactoring Refinement Structures of Event-B Machines ( abstract )

Finding Suitable Variability Abstractions for Family-Based Analysis ( abstract )

Counter-Example Guided Program Verification ( abstract )

Decoupled simulating abstractions of non-linear ordinary differential equations ( abstract )

SpecCert: Specifying and Verifying Hardware-based Security Enforcement ( abstract )

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor ( abstract )

Automated Verification of Timed Security Protocols with Clock Drift ( abstract )

Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow ( abstract )

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor ( abstract )

Formalising and Validating the Interface Description in the FMI standard ( abstract )

Equivalence Checking of a Floating-point Unit Against a High-level C Model ( abstract )

An Implementation of Deflate in Coq ( abstract )