Programmed strategies for program verification

DOI10.1016/J.ENTCS.2007.02.045MaRDI QIDQ2864527zbMATH OpenOpenAlexFDO

Authors Richard B. Kieburtz

Publication date 6 December 2013

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

Full work available at URL https://doi.org/10.1016/j.entcs.2007.02.045

zbMATH Keywords

verificationnormal formsreductiontheorem provingrewritingdecision proceduresstrategiesHaskellStratego

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• A mechanical analysis of program verification strategies
• Verification of procedural programs
• Problem-oriented program verification
• A new approach to program verification
• A unified approach of program verification
• Program verification by coinduction
• Tactical theorem proving in program verification
• scientific article; zbMATH DE number 4024753

Cites work

• scientific article; zbMATH DE number 1696759 (Why is no real title available?)
• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 1722718 (Why is no real title available?)
• scientific article; zbMATH DE number 4030948 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 2043522 (Why is no real title available?)
• scientific article; zbMATH DE number 1794375 (Why is no real title available?)
• scientific article; zbMATH DE number 2086496 (Why is no real title available?)
• scientific article; zbMATH DE number 2090060 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A framework for defining logics
• Introduction to algorithms
• Isabelle/HOL. A proof assistant for higher-order logic
• On Shostak's decision procedure for combinations of theories
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
• Simplification by Cooperating Decision Procedures
• Simplify: a theorem prover for program checking
• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• The calculus of constructions

Cited in

(2)

• Automatic Strategy Verification for Hex
• A mechanical analysis of program verification strategies

Describes a project that uses

Uses Software

• LOOP
• Sparkle
• NQTHM
• ESC/Java
• Maude
• HOL
• SIMPLIFY
• Haskell
• PVS
• ATERM
• Isabelle/HOL
• CLEAN
• Stratego
• ML
• Coq

This page was built for publication: Programmed strategies for program verification

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