Expander2: program verification between interaction and automation

DOI10.1016/J.ENTCS.2007.01.003MaRDI QIDQ2873787zbMATH OpenOpenAlexFDO

Authors Peter Padawitz

Publication date 24 January 2014

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.01.003

zbMATH Keywords

modal logicstheorem provingtransition systemsrewritingprogram verificationconstraint solvingalgebraic and coalgebraic specification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Recommendations

• Formal Methods in Software and Systems Modeling
• Swinging types=functions+relations+transition systems
• scientific article; zbMATH DE number 177262
• The algebra of expansion
• scientific article; zbMATH DE number 4047196

Cites work

• scientific article; zbMATH DE number 1566503 (Why is no real title available?)
• scientific article; zbMATH DE number 193539 (Why is no real title available?)
• scientific article; zbMATH DE number 1064116 (Why is no real title available?)
• scientific article; zbMATH DE number 1973125 (Why is no real title available?)
• scientific article; zbMATH DE number 2043522 (Why is no real title available?)
• scientific article; zbMATH DE number 1368956 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• A hidden agenda
• A needed narrowing strategy
• Algebraic-coalgebraic specification in CoCasl.
• An approach to object semantics based on terminal co-algebras
• CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
• Deduction and Declarative Programming
• Formal Methods in Software and Systems Modeling
• Inductive theorem proving for design specifications
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Isabelle/HOL. A proof assistant for higher-order logic
• Monad-independent dynamic logic in HasCasl.
• Polymorphic subtyping in O'Haskell
• Swinging types=functions+relations+transition systems

Cited in

(1)

• Formal Methods in Software and Systems Modeling

Describes a project that uses

Uses Software

• EXPANDER
• CoCasl
• Curry
• Maude
• HasCasl

This page was built for publication: Expander2: program verification between interaction and automation

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