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

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

S. De Gouw ; F. De Boer ; Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; R. Bubel
Software and Systems Modeling (1619-1366). Vol. 15 (2016), 4, p. 1117-1140.
[Artikel, refereegranskad vetenskaplig]

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.

Nyckelord: Dynamic logic, Object creation, Program logic, Specification, Verification



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-01-07. Senast ändrad 2016-11-11.
CPL Pubid: 230100

 

Läs direkt!


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