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

Lingva: Generating and proving program properties using symbol elimination

I. Dragan ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science, Perspectives of System Informatics, 9th International Ershov Informatics Conference, PSI 2014 St. Petersburg, Russia, June 24–27, 2014 (0302-9743). Vol. 8974 (2015), p. 67-75.
[Konferensbidrag, refereegranskat]

We describe the Lingva tool for generating and proving complex program properties using the recently introduced symbol elimination method. We present implementation details and report on a large number of experiments using academic benchmarks and open-source software programs. Our experiments show that Lingva can automatically generate quantified invariants, possibly with alternation of quantifiers, over integers and arrays. Moreover, Lingva can be used to prove program properties expressing the intended behavior of programs.

Nyckelord: Computer software, Information science, Open systems, Software engineering, Complex programs, Elimination method, Open source software projects, Program properties, Open source software



Denna post skapades 2015-11-16. Senast ändrad 2015-11-16.
CPL Pubid: 225817

 

Läs direkt!


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