Supplementary Web Pages
For Research Articles
- A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module (tdx-module-firmware-verification)
- A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification (dar-ismc-transferability)
- A Unifying View on SMT-based Software Verification (k-ind-compare)
- Algorithms for Software Model Checking: Predicate Abstraction vs. Impact (cpa-uni)
- Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (imc-df)
- BDD-Based Software Verification (cpa-bdd)
- Boosting k‑Induction with Continuously‑Refined Invariants (cpa-k-induction)
- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator (btor2c)
- Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers (btor2-cert)
- Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking (btor2-select)
- CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification (cpa-df)
- CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers (cpa-daemon)
- CPAchecker: A Tool for Configurable Software Verification (cpa-tool)
- CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering – (energy-measurement)
- CoVeriTeam: On-Demand Composition of Cooperative Verification Systems (coveriteam)
- CoVeriTest: Cooperative Verifier-Based Testing (coop-testgen)
- Conditional Model Checking (cpa-cmc)
- Conditional Testing (conditional-testing)
- Construction of Verifier Combinations From Off-the-Shelf Components (coveriteam-combinations)
- Cooperative Verification via Conditional Model Checking (cmc-reducers-slicers)
- Correctness Witnesses: Exchanging Verification Results between Verifiers (correctness-witnesses)
- Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR (component-based-cegar)
- DescribErr: Precise Error Conditions (describerr)
- Difference Verification with Conditions (difference)
- Distributed Summary Synthesis (distributed-summary-synthesis)
- Domain Types: Selecting Abstractions Based on Variable Usage (domaintypes)
- Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization (bam-interprocedural)
- Domain-Independent Multi-threaded Software Model Checking (bam-parallel)
- Execution-Based Validation of Violation Witnesses (executionbasedwitnessvalidation)
- Explicit-Value Analysis Based on CEGAR and Interpolation (cpa-explicit)
- FRed: Conditional Model Checking via Reducers and Folders (fred)
- Fault Localization on Witnesses (fl-witnesses)
- In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching (bam-cow-refinement)
- Information Reuse for Multi-goal Reachability Analyses (cpa-tiger)
- Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification (cpa-imc)
- LIV: Loop-Invariant Validation using Straight-Line Programs (liv)
- MoXIchecker: An Extensible Model Checker for MoXI (moxichecker)
- Non-termination Witnesses and Their Validation (non-termination-witnesses)
- On-The-Fly Decomposition of Specifications in Software Model Checking (spec-decomposition)
- Predicate Abstraction with Adjustable-Block Encoding (cpa-abe)
- Reducer-Based Construction of Conditional Verifiers (reducer)
- Refinement Selection (cpa-ref-sel)
- Reliable Benchmarking: Requirements and Solutions (benchmarking)
- Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses (cpa-reuse-gen)
- Reusing Precisions for Efficient Regression Verification (cpa-reuse)
- Software Model Checking via Large-Block Encoding (cpa-lbe)
- Software Verification in the Google App-Engine Cloud (cpa-appengine)
- Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art (pdr-compare)
- Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach (strategy-selection)
- Supplementary webpage for the paper "A Formal Evaluation of DepDegree Based on Weyuker’s Properties" (DepDegreeProperties)
- Symbolic Execution using CEGAR (cpa-symexec)
- Testing vs. Model Checking (test-study)
- Unifying Approach for Control-Flow-Based Loop Abstraction (loop-abstraction)
- Verification Witnesses Version 2 (verification-witnesses-v2)
- Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses (witness-based-debugging)
- Violation Witnesses and Result Validation for Multi-Threaded Programs (witnesses-concurrency)
- Witness Validation and Stepwise Testification across Software Verifiers (verification-witnesses)
- (cegar-pt)
- (cooperation-automatic-interactive)
- (test-to-witness)
For PhD Theses
- Effective Approaches to Abstraction Refinement for Automatic Software Verification (loewe)
- Towards Practical Predicate Analysis (wendler)