Programmed strategies for program verification

DOI10.1016/J.ENTCS.2007.02.045zbMATH Open1277.68057OpenAlexW2072047622MaRDI QIDQ2864527FDOQ2864527

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

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

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)

Cites Work

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

Cited In (2)

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

Uses Software

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

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)