TACAS 2018
54 papers
- 2LS: Memory Safety and Non-termination - (Competition Contribution)
- A Non-linear Arithmetic Procedure for Control-Command Software Verification
- A Statistical Model Checker for Nondeterminism and Rare Events
- A Verified Implementation of the Bounded List Container
- AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic
- Abstraction Refinement for Emptiness Checking of Alternating Data Automata
- Accelerating Syntax-Guided Invariant Synthesis
- Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
- Automatic Generation of Precise and Useful Commutativity Conditions
- Automating Deductive Verification for Weak-Memory Programs
- Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
- Bit-Vector Model Counting Using Statistical Estimation
- CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving
- CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis - (Competition Contribution)
- Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
- Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets
- Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper)
- EMME: A Formal Tool for ECMAScript Memory Model Evaluation
- Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
- Efficient Verification of Imperative Programs Using Auto2
- Feature-Guided Black-Box Safety Testing of Deep Neural Networks
- Fine-Grained Complexity of Safety Verification
- Frame Inference for Inductive Entailment Proofs in Separation Logic
- From Natural Projection to Partial Model Checking and Back
- Generation of Minimum Tree-Like Witnesses for Existential CTL
- Geometric Nontermination Arguments
- Hoare Logics for Time Bounds - A Study in Meta Theory
- ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
- InterpChecker: Reducing State Space via Interpolations - (Competition Contribution)
- Invariant Synthesis for Incomplete Verification Engines
- Map2Check Using LLVM and KLEE - (Competition Contribution)
- More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 )
- Multi-cost Bounded Reachability in MDP
- Oink: An Implementation and Evaluation of Modern Parity Game Solvers
- Optimal Dynamic Partial Order Reduction with Observers
- Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks
- Permutation Games for the Weakly Aconjunctive \mu μ -Calculus
- Property Checking Array Programs Using Loop Shrinking
- RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
- Revisiting Enumerative Instantiation
- SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution)
- Strategy Representation by Decision Trees in Reactive Synthesis
- Structurally Defined Conditional Data-Flow Static Analysis
- Symmetry Reduction for the Local Mu-Calculus
- TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
- The Refinement Calculus of Reactive Systems Toolset
- Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution)
- Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution)
- Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
- Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
- VeriAbs: Verification by Abstraction and Test Generation - (Competition Contribution)
- Verified Model Checking of Timed Automata
- What a Difference a Variable Makes
- YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement - (Competition Contribution)