Linked e-resources
Details
Table of Contents
Concurrent and Distributed Systems
Computing the concurrency threshold of sound free-choice workflow nets
Fine-Grained Complexity of Safety Verification
Parameterized verification of synchronization in constrained reconfigurable broadcast networks
EMME: a formal tool for the ECMAScript Memory Model Evaluation
SAT and SMT II
What a Difference a Variable Makes
Abstraction Refinement for Emptiness Checking of Alternating Data Automata
Revisiting Enumerative Instantiation
An Non-linear Arithmetic Procedure for Control-Command Software Verification
Security and Reactive Systems
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
The Refinement Calculus of Reactive Systems Toolset
Static and Dynamic Program Analysis
TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
Optimal Dynamic Partial Order Reduction with Observers
Structurally Defined Conditional Data-flow Static Analysis
Geometric Nontermination Arguments
Hybrid and Stochastic Systems
Efficient dynamic error reduction for hybrid systems reachability analysis
AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic
Multi-Cost Bounded Reachability in MDPs
A Statistical Model Checker for Nondeterminism and Rare Events
Temporal logic and mu-calculus
Permutation Games for the Weakly Aconjunctive mu-Calculus
Symmetry Reduction for the Local Mu-Calculus
Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
7th Competition on Software Verification (SV-COMP)
2LS: Memory Safety and Non-Termination (Competition contribution)
Yogar-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement (Competition Contribution)
CPA-BAM-Slicing: Block-Abstraction Memorization and Slicing with Region-Based Dependency Analysis (Competition Contribution)
InterpChecker: Reducing State Space via Interpolations (Competition Contribution)
Map2Check using LLVM and KLEE (Competition Contribution)
Symbiotic 5: Boosted Instrumentation (Competition Contribution)
Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution)
Ultimate Taipan with Dynamic Block Encoding (Competition Contribution)
VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution).
Computing the concurrency threshold of sound free-choice workflow nets
Fine-Grained Complexity of Safety Verification
Parameterized verification of synchronization in constrained reconfigurable broadcast networks
EMME: a formal tool for the ECMAScript Memory Model Evaluation
SAT and SMT II
What a Difference a Variable Makes
Abstraction Refinement for Emptiness Checking of Alternating Data Automata
Revisiting Enumerative Instantiation
An Non-linear Arithmetic Procedure for Control-Command Software Verification
Security and Reactive Systems
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
The Refinement Calculus of Reactive Systems Toolset
Static and Dynamic Program Analysis
TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
Optimal Dynamic Partial Order Reduction with Observers
Structurally Defined Conditional Data-flow Static Analysis
Geometric Nontermination Arguments
Hybrid and Stochastic Systems
Efficient dynamic error reduction for hybrid systems reachability analysis
AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic
Multi-Cost Bounded Reachability in MDPs
A Statistical Model Checker for Nondeterminism and Rare Events
Temporal logic and mu-calculus
Permutation Games for the Weakly Aconjunctive mu-Calculus
Symmetry Reduction for the Local Mu-Calculus
Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
7th Competition on Software Verification (SV-COMP)
2LS: Memory Safety and Non-Termination (Competition contribution)
Yogar-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement (Competition Contribution)
CPA-BAM-Slicing: Block-Abstraction Memorization and Slicing with Region-Based Dependency Analysis (Competition Contribution)
InterpChecker: Reducing State Space via Interpolations (Competition Contribution)
Map2Check using LLVM and KLEE (Competition Contribution)
Symbiotic 5: Boosted Instrumentation (Competition Contribution)
Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution)
Ultimate Taipan with Dynamic Block Encoding (Competition Contribution)
VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution).