Abstract interpretation from Büchi automata

DOI10.1145/2603088.2603127MaRDI QIDQ4635636zbMATH OpenOpenAlexFDO

Authors Martin Hofmann, Wei Chen

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/19353649/Hofmann_Chen_2014_Abstract_interpretation_from_buchi_automata.pdf

zbMATH Keywords

livenesstemporal propertiestype systemstype-and-effect systems

Mathematics Subject Classification ID

Galois correspondences, closure operators (in relation to ordered sets) (06A15) Structure theory of lattices (06B05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Abstract data types; algebraic specification (68Q65)

Recommendations

• Abstract interpretation as automated deduction
• Abstract Interpretation as Automated Deduction
• Abstract interpretation from a denotational-semantics perspective
• From operational semantics to abstract machines
• Determinization of Büchi-Automata
• scientific article; zbMATH DE number 1836353
• Verification, Model Checking, and Abstract Interpretation
• THE ABSTRACT THEORY OF AUTOMATA
• scientific article; zbMATH DE number 1949621
• scientific article; zbMATH DE number 1512707

Cited in

(9)

• Temporal refinements for guarded recursive types
• Abstract Interpretation as Automated Deduction
• Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification
• Enforcing Programming Guidelines with Region Types and Effects
• Domains for Higher-Order Games
• Calculational design of a regular model checker by abstract interpretation
• Automated temporal verification for algebraic effects
• Temporal verification of programs via first-order fixpoint logic
• Infinitary refinement types for temporal properties in Scott domains

This page was built for publication: Abstract interpretation from Büchi automata

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