Proving Safety with Trace Automata and Bounded Model Checking

DOI10.1007/978-3-319-19249-9_21zbMath1427.68047arXiv1410.5764OpenAlexW2963707299WikidataQ62040429 ScholiaQ62040429MaRDI QIDQ5206955

No author found.

Publication date: 19 December 2019

Published in: FM 2015: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1410.5764

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Proving Safety with Trace Automata and Bounded Model Checking

Cites Work

• Unnamed Item
• Unnamed Item
• Under-approximating loops in C programs for fast counterexample detection
• Verification and falsification of programs with loops using predicate abstraction
• Refinement of Trace Abstraction
• Fluid Updates: Beyond Strong vs. Weak Updates
• Fast Acceleration of Ultimately Periodic Relations
• Accelerating Interpolants
• Lazy abstraction
• Proving Safety with Trace Automata and Bounded Model Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Lazy Abstraction with Interpolants

This page was built for publication: Proving Safety with Trace Automata and Bounded Model Checking