An algebraic framework for abstract model checking

DOI10.1007/3-540-45622-8_12MaRDI QIDQ4737589zbMATH OpenFDO

Authors Andreas Podelski, Supratik Mukhopadhyay

Publication date 11 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2371/23710152.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Compositional termination analysis of symbolic forward analysis
• Beyond region graphs: Symbolic forward analysis of timed automata
• Symbolic model checking in non-Boolean domains
• The algorithmic analysis of hybrid systems
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation

Cited in

(10)

• A symbolic semantics for abstract model checking
• A generalized semantics of PROMELA for abstract model checking
• A proof theory for model checking
• Alias analysis by means of a model checker
• Algorithmic algebraic model checking. III: Approximate methods
• AlPiNA: A Symbolic Model Checker
• Compositional termination analysis of symbolic forward analysis
• Computer Aided Verification
• scientific article; zbMATH DE number 5181785 (Why is no real title available?)
• Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker

Describes a project that uses

Uses Software

• HyTech
• Kronos
• Uppaal

This page was built for publication: An algebraic framework for abstract model checking

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