scientific article; zbMATH DE number 2217740

zbMATH Open1073.68897MaRDI QIDQ5699474FDOQ5699474

Authors: Laura Kovács, Tudor Jebelean 

Publication date: 26 October 2005

Title of this publication is not available (Why is that?)

Recommendations

• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
• Problem-oriented program verification system ?SPEKTR?
• On automated program construction and verification
• Recent advances in program verification through computer algebra
• scientific article; zbMATH DE number 4024753

zbMATH Keywords

VerificationInvariantSymbolic ComputationProgram AnalysisWeakest Precondition

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (5)

• Efficient verification of imperative programs using auto2
• Characteristic formulae for the verification of imperative programs
• Computer Aided Verification
• Theories for mechanical proofs of imperative programs
• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}

Uses Software

• Theorema
• SPARK

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 Q5699474)