scientific article; zbMATH DE number 3748393

MaRDI QIDQ3932277zbMATH OpenFDO

Authors

Publication date 1981

zbMATH Keywords

computational logicconcurrent programsFORTRANmetatheoryprogram correctnessprogram specificationtemporal logicverification condition generator

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited in

(16)

• Integrating external deduction tools with ACL2
• Fair Petri nets and structural induction for rings of processes
• Incorporating quotation and evaluation into Church's type theory
• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• Verifying autonomous systems
• Verification of concurrent programs: The automata-theoretic framework
• Milestones from the Pure Lisp Theorem Prover to ACL2
• From model checking to equilibrium checking: reactive modules for rational verification
• Tactics for Reasoning Modulo AC in Coq
• Reflection of formal tactics in a deductive reflection framework
• Verification conditions for source-level imperative programs
• Formal Proofs for Nonlinear Optimization
• A theorem prover for a computational logic
• Temporal precondition verification of design transformations
• Rod Burstall: in memoriam (1934--2025)
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

This page was built for publication:

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