Tools and Algorithms for the Construction and Analysis of Systems

DOI10.1007/b107194zbMath1087.68586OpenAlexW2497867240MaRDI QIDQ5703792

Karen Yorav, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke

Publication date: 10 November 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

Related Items (21)

Model-Checking HyperLTL for Pushdown Systems ⋮ Splitting via Interpolants ⋮ Verification of SpecC using predicate abstraction ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Interpolation and Model Checking ⋮ Predicate Abstraction for Program Verification ⋮ Context-aware counter abstraction ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ Efficient strategies for CEGAR-based model checking ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Loop Summarization and Termination Analysis ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Loop summarization using state and transition invariants ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ Counterexample Guided Path Reduction for Static Program Analysis ⋮ Temporalization of Probabilistic Propositional Logic ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ Automatic analysis of DMA races using model checking and \(k\)-induction ⋮ Automated formal analysis and verification: an overview

Uses Software

• ComFoRT
• SatAbs

This page was built for publication: Tools and Algorithms for the Construction and Analysis of Systems