A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
Abstract elided by the publisher.
1,553 papers · page 39 of 78
LTSmin: High-Performance Language-Independent Model Checking
Abstract elided by the publisher.
Limit Deterministic and Probabilistic Automata for LTL ∖ GU
Abstract elided by the publisher.
dReach: δ-Reachability Analysis for Hybrid Systems
Abstract elided by the publisher.
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
Abstract elided by the publisher.
Value Slice: A New Slicing Concept for Scalable Property Checking
Abstract elided by the publisher.
Saturation-Based Incremental LTL Model Checking with Inductive Proofs
Abstract elided by the publisher.
Predator Hunting Party (Competition Contribution)
Abstract elided by the publisher.
Analysis of Dynamic Process Networks
Abstract elided by the publisher.
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution)
Abstract elided by the publisher.
ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution)
Abstract elided by the publisher.
MarQ: Monitoring at Runtime with QEA
Abstract elided by the publisher.
Parallel Explicit Model Checking for Generalized Büchi Automata
Abstract elided by the publisher.
Symbolic Quantitative Robustness Analysis of Timed Automata
We study the robust safety problem for timed automata under guard imprecisions which consists in computing an imprecision parameter under which a safety specification holds. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its p…
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories SMT solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of…
FAUST 2 : Formal Abstractions of Uncountable-STate STochastic Processes
FAUST $^{\mathsf 2}$ is a software tool that generates formal abstractions of possibly non-deterministic discrete-time Markov processes dtMP defined over uncountable continuous state spaces. A dtMP model is specified in MATLAB and abstracted as a finite-state Markov chain or a Ma…
AProVE: Termination and Memory Safety of C Programs - (Competition Contribution)
Abstract elided by the publisher.
Symbolic Model-Checking Using ITS-Tools
Abstract elided by the publisher.
MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution)
Abstract elided by the publisher.
Verifying Concurrent Programs by Memory Unwinding
Abstract elided by the publisher.