Automated Program Verification

DOI10.1007/978-3-319-15579-1_2zbMath1451.68175OpenAlexW1897875017MaRDI QIDQ2799160

Jochen Hoenicke, Matthias Heizmann, Andreas Podelski, Azadeh Farzan, Zachary Kincaid

Publication date: 8 April 2016

Published in: Language and Automata Theory and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-15579-1_2

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Finite-memory automata
• Proof Spaces for Unbounded Parallelism
• Alternating register automata on finite words and trees
• Inductive data flow graphs
• LTL with the freeze quantifier and register automata
• Refinement of Trace Abstraction
• Adding nesting structure to words
• Precise interprocedural dataflow analysis with applications to constant propagation
• Linear Ranking for Linear Lasso Programs
• Nested interpolants
• Finite state machines for strings over infinite alphabets
• Proof Tree Preserving Interpolation
• Proofs that count
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Automated Program Verification