CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Specifying Imperative ML-like Programs Using Dynamic Logic

Severine Maingaud ; Vincent Balat ; Richard Bubel (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Reiner Hähnle (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Alexandre Miquel
Lecture Notes in Computer Science. International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010, Paris, 28-30 June 2010 (0302-9743). Vol. 6528 (2011), p. 122-137.
[Konferensbidrag, refereegranskat]

We present a logical system suited for specification and verification of imperative ML programs. The specification language combines dynamic logic (DL), explicit state updates and second-order functional arithmetic. Its proof system is based on a Gentzen-style sequent calculus (adapted to modal logic) with facilities for symbolic evaluation. We illustrate the system with some example, and give a full Kripke-style semantics in order to prove its correctness.

Nyckelord: AF2; dynamic logic; KeY; ML; program specification; program verification



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2010-10-27. Senast ändrad 2016-07-26.
CPL Pubid: 128193

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)