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

A formalisation of Java Strings for program specification and verification

Richard Bubel (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Reiner Hähnle (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; U. Geilmann
Lecture Notes in Computer Science. 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, Montevideo, 14-18 November 2011 (0302-9743). Vol. 7041 (2011), p. 90-105.
[Konferensbidrag, refereegranskat]

We present a formalisation of Java Strings tailored to specification and verification of programs (using dynamic logic). The formalism allows to specify and verify properties about the content of strings-the most common use-case-in an easy and natural manner. Each instance of type String is related to an abstract data type representing the string content as an immutable sequence of characters. This avoids serious technicalities that would arise if the specification had to resort to Java arrays to represent sequences of characters. We also discuss advanced aspects of Java Strings including string literals and the string pool and support for regular expressions. The approach has been implemented in the KeY verification system. We demonstrate its practical applicability by case studies including the verification of a string sanitization function.



Denna post skapades 2012-02-07. Senast ändrad 2016-07-26.
CPL Pubid: 154851

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Information Technology

Chalmers infrastruktur