Tools and Algorithms for the Construction and Analysis of Systems - Dirk Beyer

. .

Résumé :
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-BasedDependency 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)....

Sommaire:

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-BasedDependency 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).