4 papers · 1 filter
Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs
Po-Chun Chien, Nian-Ze Lee, Armin Biere +1
Formal verification of software programs and hardware designs shares the common goal of reasoning about state-transition systems, yet the two communities have largely developed sep…
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
Dirk Beyer, Po-Chun Chien, Nian-Ze Lee
Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtain…
Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
Daniel Baier, Dirk Beyer, Po-Chun Chien +8
This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides ma…
MoXIchecker: An Extensible Model Checker for MoXI
Salih Ates, Dirk Beyer, Po-Chun Chien +1
MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-…