Abstracting models from execution traces for performing formal verification

DOI10.1007/978-3-642-10619-4_18MaRDI QIDQ5305770zbMATH OpenOpenAlexFDO

Authors Thierry Bodhuin, Federico Pagnozzi, Antonella Santone, Maria Tortorella, Maria Luisa Villani

Publication date 23 March 2010

Published in Advances in Software Engineering (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-10619-4_18

zbMATH Keywords

bytecodeCCSmodel checkingruntime instrumentation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Software model checking
• scientific article; zbMATH DE number 1633145
• scientific article; zbMATH DE number 2087639
• Model Checking Software
• Formal Methods at the Crossroads. From Panacea to Foundational Support

Cites work

• A transformation system for concurrent processes
• A Transformation System for Developing Recursive Programs
• Abstracting models from execution traces for performing formal verification
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Selective mu-calculus and formula-based equivalence of transition systems
• Transformation of logic programs: Foundations and techniques

Cited in

(2)

• Verification of compliance for multilevel models in individual trace semantics
• Abstracting models from execution traces for performing formal verification

This page was built for publication: Abstracting models from execution traces for performing formal verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5305770)