Simplification of boolean verification conditions

DOI10.1016/S0304-3975(99)00217-0zbMath0944.68126MaRDI QIDQ1575276

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)

Uses Software

• UNITY
• STeP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Concurrency without toil: A systematic method for parallel program design
• An assertional correctness proof of a distributed algorithm
• A verification system for concurrent programs based on the Boyer-Moore prover
• Introduction to the OBDD algorithm for the ATP community
• A mechanically verified incremental garbage collector
• Automatic generation of invariants and intermediate assertions
• Model theory
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Programming as a Discipline of Mathematical Nature

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