Extended Static Checking by Calculation Using the Pointfree Transform

DOI10.1007/978-3-642-03153-3_5zbMath1250.68093MaRDI 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 methods; extended static checking; proof obligations

Mathematics Subject Classification ID

03B70: Logic in computer science

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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

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