Title :
Formal verification applied to Java concurrent software
Author_Institution :
Dipt. di Autom., Politecnico di Torino, Italy
Abstract :
Applying existing finite-state verification tools to software systems is not yet easy for a variety of reasons. The research activity presented aims to integrate formal verification with programming languages currently used in software development. In particular, it focuses on elaborating a formal method for the specification and validation of temporal logic properties concerning the behavior of Java concurrent programs
Keywords :
Java; finite state machines; formal specification; parallel programming; program verification; temporal logic; Java concurrent programs; Java concurrent software; finite-state verification tools; formal method; formal verification; programming languages; research activity; software systems; specification; temporal logic properties; Computer languages; Concurrent computing; Formal verification; Java; Logic programming; Memory management; Reasoning about programs; Software engineering; Software systems; System recovery;
Conference_Titel :
Software Engineering, 2000. Proceedings of the 2000 International Conference on
Conference_Location :
Limerick
Print_ISBN :
1-58113-206-9
DOI :
10.1109/ICSE.2000.870475
