Efficient bounded model checking of heap-manipulating programs using tight field bounds

DOI10.1007/978-3-030-71500-7_11zbMath1467.68092OpenAlexW3135988295MaRDI QIDQ2044185

Yanyan Li

Publication date: 4 August 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-71500-7_11

Mathematics Subject Classification ID

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

Uses Software

• MiniSat
• Korat
• Java PathFinder
• TACO
• LLBMC
• CBMC
• JPF-SE
• YOGI
• DynAlloy

Cites Work

• Unnamed Item
• Unnamed Item
• Solving the incremental satisfiability problem
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• Shape Analysis for Composite Data Structures
• Automated Verification of Shape and Size Properties Via Separation Logic
• Automated Technology for Verification and Analysis
• Computer Aided Verification
• Bounded model checking using satisfiability solving

This page was built for publication: Efficient bounded model checking of heap-manipulating programs using tight field bounds