Calculational design of a regular model checker by abstract interpretation

DOI10.1016/J.TCS.2021.01.037MaRDI QIDQ5896884zbMATH OpenOpenAlexFDO

Authors Patrick Cousot

Publication date 10 May 2021

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2021.01.037

zbMATH Keywords

model checkingabstract interpretationcalculational design

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1390341
• An abstract interpretation-based model for safety semantics
• scientific article; zbMATH DE number 1948413
• scientific article; zbMATH DE number 1798181
• scientific article; zbMATH DE number 1059247

Cites work

• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 45231 (Why is no real title available?)
• scientific article; zbMATH DE number 3459853 (Why is no real title available?)
• scientific article; zbMATH DE number 3463159 (Why is no real title available?)
• scientific article; zbMATH DE number 1487852 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 1759702 (Why is no real title available?)
• scientific article; zbMATH DE number 1834576 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 3253940 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Abstract interpretation from Büchi automata
• Automata theory and model checking
• CONCUR 2004 - Concurrency Theory
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Constructive versions of Tarski's fixed point theorems
• Derivatives of Regular Expressions
• Derivatives of quantitative regular expressions
• Elements of automata theory. Translated from the French by Reuben Thomas
• Graph-Based Algorithms for Boolean Function Manipulation
• Handbook of model checking
• Incompleteness of states w.r.t. traces in model checking
• Model-checking in-lined reference monitors
• Process logic: Expressiveness, decidability, completeness
• Quantifiers on languages and codensity monads
• Regular-expression derivatives re-examined
• Saving space in a time efficient simulation algorithm
• Symbolic execution and program testing
• Temporal abstract interpretation
• Temporal logic can be more expressive
• “Sometimes” and “not never” revisited

Cited in

(3)

• Exploiting design structure in model checking. (Abstract)
• An abstract interpretation-based model for safety semantics
• scientific article; zbMATH DE number 1390341 (Why is no real title available?)

Describes a project that uses

Uses Software

• CESAR
• SLAM

This page was built for publication: Calculational design of a regular model checker by abstract interpretation

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