Computer Science Logic

DOI10.1007/11538363MaRDI QIDQ5394591zbMATHOpenAlexFDO

Authors Witold Charatonik, Lilia Georgieva, Patrick Maier

Publication date 1 November 2006

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

Full work available at URL https://doi.org/10.1007/11538363

Mathematics Subject Classification ID

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

Recommendations

• Bounded model checking of recursive programs with pointers in K
• Efficient modular SMT-based model checking of pointer programs
• Computer Aided Verification
• Symbolic bounded conformance checking of model programs
• Pointer logic for verification of pointer programs
• Completeness and expressiveness of pointer program verification by separation logic
• Bounded model checking with parametric data structures
• scientific article; zbMATH DE number 1979554

Cited in

(10)

• Unbounded allocation in bounded heaps
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Using unified model checking to verify heaps
• Efficient modular SMT-based model checking of pointer programs
• Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic
• Bounded model checking of recursive programs with pointers in K
• Convergence testing in term-level bounded model checking
• Two-variable logic with counting and trees
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Towards Model-Checking Programs with Lists

This page was built for publication: Computer Science Logic

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