Expander2: Program Verification Between Interaction and Automation

DOI10.1016/j.entcs.2007.01.003zbMath1279.68293OpenAlexW2077898879MaRDI QIDQ2873787

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

theorem provingrewritingtransition systemsmodal logicsconstraint solvingprogram verificationalgebraic and coalgebraic specification

Mathematics Subject Classification ID

Uses Software

• HasCasl
• Maude
• Curry
• CoCasl
• EXPANDER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Polymorphic subtyping in O'Haskell
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• CASL user manual. Introduction to using the Common Algebraic Specification Language. With chapters by Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. With CD-ROM.
• Swinging types=functions+relations+transition systems
• A hidden agenda
• Isabelle/HOL. A proof assistant for higher-order logic
• Inductive theorem proving for design specifications
• A needed narrowing strategy
• Deduction and Declarative Programming
• An approach to object semantics based on terminal co-algebras
• Formal Methods in Software and Systems Modeling
• Recent Trends in Algebraic Development Techniques
• Recent Trends in Algebraic Development Techniques

This page was built for publication: Expander2: Program Verification Between Interaction and Automation