Article

Free access

Bandera: a source-level interface for model checking Java programs

Authors:

James C. Corbett,

Matthew B. Dwyer,

John Hatcliff,

RobbyAuthors Info & Claims

ICSE '00: Proceedings of the 22nd international conference on Software engineering

Pages 762 - 765

https://doi.org/10.1145/337180.337625

Published: 01 June 2000 Publication History

PDF eReader

Abstract

Despite emerging tool support for assertion-checking and testing of object-oriented programs, providing convincing evidence of program correctness remains a difficult challenge. This is especially true for multi-threaded programs. Techniques for reasoning about finite-state systems have been developing rapidly over the past decade and have the potential to form the basis of powerful software validation theologies.

We have developed the Bandera toolset [1] to harness the power of existing model checking tools to apply them to reason about correctness requirements of Java programs. Bandera provides tool support for defining and managing collections of requirements for a program, for extracting compact finite-state models of the program to enable tractable analysis, and for displaying analysis results to the user through a debugger-like interface. This paper describes and illustrates the use of Bandera's source-level user interface for model checking Java programs.

References

[1]

J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera : Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.

Digital Library

Google Scholar

[2]

G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279{294, May 1997.

Digital Library

Google Scholar

[3]

K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

Cited By

View all

Partenza GAmburgey TDeng LDehlinger JChakraborty S(2021)Automatic Identification of Vulnerable Code: Investigations with an AST-Based Neural Network2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC)10.1109/COMPSAC51774.2021.00219(1475-1482)Online publication date: Jul-2021
https://doi.org/10.1109/COMPSAC51774.2021.00219
Daszczuk W(2021)Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3)Software and Systems Modeling10.1007/s10270-021-00917-7Online publication date: 1-Nov-2021
https://doi.org/10.1007/s10270-021-00917-7
Webster MWestern DAraiza-Illan DDixon CEder KFisher MPipe A(2019)A corroborative approach to verification and validation of human–robot teamsThe International Journal of Robotics Research10.1177/0278364919883338(027836491988333)Online publication date: 25-Nov-2019
https://doi.org/10.1177/0278364919883338
Show More Cited By

Index Terms

Bandera: a source-level interface for model checking Java programs
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Bandera: extracting finite-state models from Java source code
ICSE '00: Proceedings of the 22nd international conference on Software engineering

Finite-state verification techniques, such as model checking, have shown promise as a cost-effective means for finding defects in hardware designs. To date, the application of these techniques to software has been hindered by several obstacles. Chief ...
Correctness witnesses: exchanging verification results between verifiers
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Standard verification tools provide a counterexample to witness a specification violation, and, since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the ...
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '00: Proceedings of the 22nd international conference on Software engineering

June 2000

843 pages

ISBN:1581132069

DOI:10.1145/337180

Chairmen:
Carlo Ghezzi
Politecnico di Milano, Milau, Italy
,
Mehdi Jazayeri
Technical Univ. of Vienna, Vienna, Austria
,
Alexander L. Wolf
Univ. of Colorado, Boulder, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE00

Sponsor:

Irish Comp Soc
SIGSOFT
IEEE-CS

ICSE00: 22nd International Conference on Software Engineering

June 4 - 11, 2000

Limerick, Ireland

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
548
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)13

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Partenza GAmburgey TDeng LDehlinger JChakraborty S(2021)Automatic Identification of Vulnerable Code: Investigations with an AST-Based Neural Network2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC)10.1109/COMPSAC51774.2021.00219(1475-1482)Online publication date: Jul-2021
https://doi.org/10.1109/COMPSAC51774.2021.00219
Daszczuk W(2021)Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3)Software and Systems Modeling10.1007/s10270-021-00917-7Online publication date: 1-Nov-2021
https://doi.org/10.1007/s10270-021-00917-7
Webster MWestern DAraiza-Illan DDixon CEder KFisher MPipe A(2019)A corroborative approach to verification and validation of human–robot teamsThe International Journal of Robotics Research10.1177/0278364919883338(027836491988333)Online publication date: 25-Nov-2019
https://doi.org/10.1177/0278364919883338
Czepa CZdun U(2019)How Understandable Are Pattern-based Behavioral Constraints for Novice Software Designers?ACM Transactions on Software Engineering and Methodology10.1145/330660828:2(1-38)Online publication date: 26-Feb-2019
https://dl.acm.org/doi/10.1145/3306608
Wen JYang GHung CPapadopoulos G(2019)Parallel property checking with staged symbolic executionProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297457(1802-1809)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297457
Saccente NDehlinger JDeng LChakraborty SXiong Y(2019)Project Achilles: A Prototype Tool for Static Method-Level Vulnerability Detection of Java Source Code Using a Recurrent Neural Network2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshop (ASEW)10.1109/ASEW.2019.00040(114-121)Online publication date: Nov-2019
https://doi.org/10.1109/ASEW.2019.00040
Wen JYang G(2017)Staged Symbolic Execution for Parallel Property CheckingACM SIGSOFT Software Engineering Notes10.1145/3011286.301129741:6(1-5)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1145/3011286.3011297
Melo SSouza SSilva RSouza PVos TEldh SPrasetya W(2015)Concurrent software testing in practice: a catalog of toolsProceedings of the 6th International Workshop on Automating Test Case Design, Selection and Evaluation10.1145/2804322.2804328(31-40)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804322.2804328
Yang GKhurshid SPerson SRungta NJalote PBriand LHoek A(2014)Property differencing for incremental checkingProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568319(1059-1070)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568319
Nguyen VRuys T(2013)Selected dynamic issues in software model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0261-y15:4(337-362)Online publication date: 1-Aug-2013
https://dl.acm.org/doi/10.1007/s10009-012-0261-y
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Bandera: extracting finite-state models from Java source code

Correctness witnesses: exchanging verification results between verifiers

Conditional model checking: a technique to pass information between verifiers