SPEEDY: An Eclipse-based IDE for invariant inference
SPEEDY is an Eclipse-based IDE for exploring techniques that assist users in generating correct specifications, particularly including invariant inference algorithms and tools. It integrates with several back-end tools that propose invariants and will incorporate published algorithms for inferring o...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1404.6605v1 |
| _version_ | 1811233478409191424 |
|---|---|
| author | David R. Cok Scott C. Johnson |
| author_facet | David R. Cok Scott C. Johnson |
| author_sort | David R. Cok |
| collection | DOAJ |
| description | SPEEDY is an Eclipse-based IDE for exploring techniques that assist users in generating correct specifications, particularly including invariant inference algorithms and tools. It integrates with several back-end tools that propose invariants and will incorporate published algorithms for inferring object and loop invariants. Though the architecture is language-neutral, current SPEEDY targets C programs. Building and using SPEEDY has confirmed earlier experience demonstrating the importance of showing and editing specifications in the IDEs that developers customarily use, automating as much of the production and checking of specifications as possible, and showing counterexample information directly in the source code editing environment. As in previous work, automation of specification checking is provided by back-end SMT solvers. However, reducing the effort demanded of software developers using formal methods also requires a GUI design that guides users in writing, reviewing, and correcting specifications and automates specification inference. |
| first_indexed | 2024-04-12T11:19:45Z |
| format | Article |
| id | doaj.art-12e39d05066545e68a6c71b511eff6b0 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T11:19:45Z |
| publishDate | 2014-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-12e39d05066545e68a6c71b511eff6b02022-12-22T03:35:23ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-04-01149Proc. F-IDE 2014445710.4204/EPTCS.149.5:7SPEEDY: An Eclipse-based IDE for invariant inferenceDavid R. CokScott C. JohnsonSPEEDY is an Eclipse-based IDE for exploring techniques that assist users in generating correct specifications, particularly including invariant inference algorithms and tools. It integrates with several back-end tools that propose invariants and will incorporate published algorithms for inferring object and loop invariants. Though the architecture is language-neutral, current SPEEDY targets C programs. Building and using SPEEDY has confirmed earlier experience demonstrating the importance of showing and editing specifications in the IDEs that developers customarily use, automating as much of the production and checking of specifications as possible, and showing counterexample information directly in the source code editing environment. As in previous work, automation of specification checking is provided by back-end SMT solvers. However, reducing the effort demanded of software developers using formal methods also requires a GUI design that guides users in writing, reviewing, and correcting specifications and automates specification inference.http://arxiv.org/pdf/1404.6605v1 |
| spellingShingle | David R. Cok Scott C. Johnson SPEEDY: An Eclipse-based IDE for invariant inference Electronic Proceedings in Theoretical Computer Science |
| title | SPEEDY: An Eclipse-based IDE for invariant inference |
| title_full | SPEEDY: An Eclipse-based IDE for invariant inference |
| title_fullStr | SPEEDY: An Eclipse-based IDE for invariant inference |
| title_full_unstemmed | SPEEDY: An Eclipse-based IDE for invariant inference |
| title_short | SPEEDY: An Eclipse-based IDE for invariant inference |
| title_sort | speedy an eclipse based ide for invariant inference |
| url | http://arxiv.org/pdf/1404.6605v1 |
| work_keys_str_mv | AT davidrcok speedyaneclipsebasedideforinvariantinference AT scottcjohnson speedyaneclipsebasedideforinvariantinference |