Calculational design of a regular model checker by abstract interpretation

DOI10.1016/J.TCS.2021.01.037zbMATH Open1497.68294OpenAlexW3127127423MaRDI QIDQ5896884FDOQ5896884

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

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

zbMATH Keywords

model checkingabstract interpretationcalculational design

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Exploiting design structure in model checking. (Abstract)
• An abstract interpretation-based model for safety semantics
• Title not available (Why is that?)

Uses Software

• SLAM
• CESAR

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)