Extended Static Checking by Calculation Using the Pointfree Transform

DOI10.1007/978-3-642-03153-3_5zbMath1250.68093OpenAlexW1519644068MaRDI QIDQ5191091

José Nuno Oliveira

Publication date: 28 July 2009

Published in: Language Engineering and Rigorous Software Development (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1822/24572

zbMATH Keywords

formal methodsextended static checkingproof obligations

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

An exercise on the generation of many-valued dynamic logics ⋮ Towards patterns for heaps and imperative lambdas ⋮ Continuity as a computational effect ⋮ Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm ⋮ Relations as Executable Specifications: Taming Partiality and Non-determinism Using Invariants ⋮ Programming from metaphorisms ⋮ Programming from Galois connections ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ An algebraic framework for minimum spanning tree problems ⋮ A linear algebra approach to OLAP

Uses Software

• ML
• Haskell
• HOL
• ESC/Java
• QuickCheck
• Galculator
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Transposing partial components--an exercise on coalgebraic refinement
• A calculational approach to mathematical induction
• Safety of abstract interpretations for free, via logical relations and Galois connections
• A mini challenge: build a verifiable filesystem
• Introduction to Coalgebra
• Exercises in Quantifier Manipulation
• Can programming be liberated from the von Neumann style?
• Demonic operators and monotype factors
• NOTES ON THE UNIVERSALITY OF RELATIONAL FUNCTORS
• Mathematics of Program Construction
• Polymorphism and separation in hoare type theory
• Calculating Invariants as Coreflexive Bisimulations
• An axiomatic basis for computer programming
• FM 2005: Formal Methods
• On Hoare logic and Kleene algebra with tests
• Galois Connexions

This page was built for publication: Extended Static Checking by Calculation Using the Pointfree Transform