Programmed Strategies for Program Verification

DOI10.1016/j.entcs.2007.02.045zbMath1277.68057OpenAlexW2072047622MaRDI QIDQ2864527

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

verificationtheorem provingreductionnormal formsrewritingHaskelldecision proceduresstrategiesStratego

Mathematics Subject Classification ID

Uses Software

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

Cites Work

• The addition of bounded quantification and partial functions to a computational logic and its theorem prover
• The calculus of constructions
• Isabelle/HOL. A proof assistant for higher-order logic
• Simplify: a theorem prover for program checking
• Simplification by Cooperating Decision Procedures
• A framework for defining logics
• On Shostak's decision procedure for combinations of theories
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Programmed Strategies for Program Verification