Simplification of boolean verification conditions

DOI10.1016/S0304-3975(99)00217-0MaRDI QIDQ1575276zbMATH OpenFDO

Authors E. Pascal Gribomont

Publication date 21 August 2000

Published in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

boolean verification conditions

Mathematics Subject Classification ID

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

Recommendations

• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Simplification in a satisfiability checker for VLSI applications
• scientific article; zbMATH DE number 1705165

Cites work

• scientific article; zbMATH DE number 4110158 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• A mechanically verified incremental garbage collector
• A verification system for concurrent programs based on the Boyer-Moore prover
• An assertional correctness proof of a distributed algorithm
• Automatic generation of invariants and intermediate assertions
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Concurrency without toil: A systematic method for parallel program design
• Graph-Based Algorithms for Boolean Function Manipulation
• Introduction to the OBDD algorithm for the ATP community
• Model theory
• Programming as a Discipline of Mathematical Nature

Cited in

(1)

• Formula normalizations in verification

Describes a project that uses

Uses Software

• STeP
• UNITY

This page was built for publication: Simplification of boolean verification conditions

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