More Web Proxy on the site http://driver.im/

research-article

Korat-API: a framework to enhance korat to better support testing and reliability techniques

Authors:

Zakaria Alrmaih,

Amresh Kulkarni,

Sarfraz KhurshidAuthors Info & Claims

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Pages 1934 - 1943

https://doi.org/10.1145/3167132.3167339

Published: 09 April 2018 Publication History

Abstract

Logical constraints play an important role in software testing and reliability. For example, constraints written by users allow automating test case generation and systematic bug finding, and constraints computed using data-flow of a program allow studying its reliability. The key to practical usefulness of constraints is the effectiveness and efficiency of constraint solvers that determine constraint feasibility and produce solutions.

Our focus in this paper is the well-studied solver Korat for constraints written as imperative predicates. We introduce Korat-API, a novel framework that introduces an API for building constraint solving problems, and algorithms for solving them to enhance Korat. Our goal is two-fold: (1) to facilitate the use of Korat as an optimized constraint solver when used as a standalone tool or as a backend engine; (2) to optimize Korat for more efficient constraint solving by exploiting problem-specific information. We describe the API and algorithms that embody our framework. We also present an experimental evaluation using a suite of complex constraint solving problems to show the potential usefulness of Korat-API.

References

[1]

Zakaria Alrmaih. 2017. Korat-API: An API for building constraint solving problems for Korat. Master's thesis. University of Texas at Austin.

[2]

Saswat Anand, Edmund K. Burke, Tsong Yueh Chen, John A. Clark, Myra B. Cohen, Wolfgang Grieskamp, Mark Harman, Mary Jean Harrold, and Phil McMinn. 2013. An orchestrated survey of methodologies for automated software test case generation. Journal of Systems and Software (2013).

Digital Library

[3]

Krzysztof R. Apt and Mark Wallace. 2007. Constraint Logic Programming Using Eclipse. Cambridge University Press.

Digital Library

[4]

Hamid Bagheri and Sam Malek. 2016. Titanium: efficient analysis of evolving Alloy specifications. In FSE.

Digital Library

[5]

Christian Bird, Venkatesh-Prasad Ranganath, Thomas Zimmermann, Nachiappan Nagappan, and Andreas Zeller. 2014. Extrinsic influence factors in software reliability: a study of 200,000 windows machines. In ICSE.

Digital Library

[6]

Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. 2002. Korat: Automated testing based on Java predicates. In ISSTA.

Digital Library

[7]

Ahmet Celik, Sreepathi Pai, Sarfraz Khurshid, and Milos Gligoric. 2017. Bounded Exhaustive Test-Input Generation on GPUs. In OOPLSA.

Digital Library

[8]

Marcello Cinque, Claudio Gaiani, Daniele De Stradis, Antonio Pecchia, Roberto Pietrantuono, and Stefano Russo. 2014. On the Impact of Debugging on Software Reliability Growth Analysis: A Case Study. In ICCSA.

[9]

Leonardo de Moura and Nikolaj Bjorner. 2008. Z3: An Efficient SMT Solver. In TACAS.

Digital Library

[10]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover. In CADE-25.

[11]

Nima Dini. 2016. MKorat: A Novel Approach for Memoizing the Korat Search and Some Potential Applications. Master's thesis. University of Texas at Austin.

[12]

Nima Dini, Cagdas Yelen, and Sarfraz Khurshid. 2017. Optimizing Parallel Korat Using Invalid Ranges. In SPIN.

[13]

Romney B. Duffey and Lance Fiondella. 2014. Software, Hardware, and Procedure Reliability by Testing and Verification: Evidence of Learning Trends. IEEE Trans. Human-Machine Systems (2014).

[14]

Niklas Een and Niklas Sorensson. 2003. An Extensible SAT-solver. In SAT.

[15]

Bassem Elkarablieh, Darko Marinov, and Sarfraz Khurshid. 2008. Efficient solving of structural constraints. In ISSTA.

Digital Library

[16]

Felipe Febrero, Coral Calero, and Maria Ángeles Moraga. 2014. A Systematic Mapping Study of Software Reliability Modeling. Information & Software Technology (2014).

[17]

Antonio Filieri, Marcelo F. Frias, Corina S. Pasareanu, and Willem Visser. 2015. Model Counting for Complex Data Structures. In SPIN.

[18]

Antonio Filieri, Corina S. Pasareanu, and Willem Visser. 2013. Reliability analysis in symbolic pathfinder. In ICSE.

Digital Library

[19]

Gordon Fraser and Andreas Zeller. 2010. Mutation-driven generation of unit tests and oracles. In ISSTA.

Digital Library

[20]

J. P. Galeotti, N. Rosner, C. G. López Pombo, and M. F. Frias. 2013. TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds. Transactions on Software Engineering (2013).

Digital Library

[21]

Carlo Ghezzi, Mauro Pezzè, and Giordano Tamburrelli. 2013. Adaptive REST applications via model inference and probabilistic model checking. In IM.

[22]

Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, and Darko Marinov. 2010. Test generation through programming in UDITA. In ICSE.

Digital Library

[23]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. In PLDI.

Digital Library

[24]

Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press.

Digital Library

[25]

Daniel Jackson and Mandana Vaziri. 2000. Finding Bugs with a Constraint Solver. In ISSTA.

Digital Library

[26]

Sarfraz Khurshid, Corina Pasareanu, and Willem Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In TACAS.

Digital Library

[27]

James C. King. 1976. Symbolic Execution and Program Testing. CACM 19, 7 (1976).

Digital Library

[28]

Kodkod applications website. 2017. http://emina.github.io/kodkod/apps.html. (2017).

[29]

KoratWebPage 2017. Korat Home Page. (2017). http://korat.sourceforge.net/index.html.

[30]

Amresh Kulkarni. 2007. Constraint Prioritization for Efficient Test Generation Using Korat. Master's thesis. University of Texas at Austin.

[31]

Barbara Liskov and John Guttag. 2000. Program Development in Java: Abstraction, Specification, and Object-Oriented Design.

Digital Library

[32]

Darko Marinov. 2004. Automatic Testing of Software with Structurally Complex Inputs. Ph.D. Dissertation. Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology.

Digital Library

[33]

Darko Marinov and Sarfraz Khurshid. 2001. TestEra: A Novel Framework for Automated Testing of Java Programs. In ASE.

Digital Library

[34]

Sasa Misailovic, Aleksandar Milicevic, Nemanja Petrovic, Sarfraz Khurshid, and Darko Marinov. 2007. Parallel test generation and execution with Korat. In FSE.

Digital Library

[35]

Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball. 2007. Feedback-Directed Random Test Generation. In ICSE.

Digital Library

[36]

N. Rosner, J. Geldenhuys, N. M. Aguirre, W. Visser, and M. F. Frias. 2015. BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support. Transactions on Software Engineering (2015).

[37]

Sina Shamshiri, René Just, José Miguel Rojas, Gordon Fraser, Phil McMinn, and Andrea Arcuri. 2015. Do Automatically Generated Unit Tests Find Real Faults? An Empirical Study of Effectiveness and Challenges (T). In ASE.

[38]

Junaid Haroon Siddiqui and Sarfraz Khurshid. 2009. PKorat: Parallel Generation of Structurally Complex Test Inputs. In ICST.

[39]

Junaid Haroon Siddiqui, Darko Marinov, and Sarfraz Khurshid. 2009. Optimizing a Structural Constraint Solver for Efficient Software Checking. In ASE.

[40]

Raghavendra Srinivasan. 2015. Improving constraint-based test input generation using Korat. Master's thesis. University of Texas at Austin.

[41]

Emina Torlak and Daniel Jackson. 2007. Kodkod: A Relational Model Finder. In TACAS.

Digital Library

[42]

Engin Uzuncaova and Sarfraz Khurshid. 2008. Constraint Prioritization for Efficient Analysis of Declarative Models. In FM.

Digital Library

[43]

Hua Zhong, Lingming Zhang, and Sarfraz Khurshid. 2016. Combinatorial generation of structurally complex test inputs for commercial software applications. In FSE.

Digital Library

Cited By

Jovanovic ASullivan A(2024)Mutation testing for temporal alloy models (extended version)Software and Systems Modeling10.1007/s10270-024-01220-xOnline publication date: 28-Oct-2024
https://doi.org/10.1007/s10270-024-01220-x
Sullivan A(2023)Integrating Testing into the Alloy Model Development Workflow2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)10.1109/MODELS58315.2023.00030(117-128)Online publication date: 1-Oct-2023
https://doi.org/10.1109/MODELS58315.2023.00030
Jovanovic ASullivan A(2023)Mutation Testing for Temporal Alloy Models2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)10.1109/MODELS58315.2023.00013(228-238)Online publication date: 1-Oct-2023
https://doi.org/10.1109/MODELS58315.2023.00013
Show More Cited By

Korat-API: a framework to enhance korat to better support testing and reliability techniques
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis

Recommendations

Korat: automated testing based on Java predicates

This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat ...
Parallel test generation and execution with Korat
ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

We present novel algorithms for parallel testing of code that takes structurally complex test inputs. The algorithms build on the Korat algorithm for constraint-based generation of structurally complex test inputs. Given an imperative predicate that ...
Transforming an under-constrained geometric constraint problem into a well-constrained one
SM '03: Proceedings of the eighth ACM symposium on Solid modeling and applications

We present an approach for handling geometric constraint problems with under-constrained configurations. The approach works by completing the given set of constraints with constraints that can be defined either automatically or drawn from an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

April 2018

2327 pages

ISBN:9781450351911

DOI:10.1145/3167132

Conference Chairs:
Hisham M. Haddad
Kennesaw State University
,
Roger L. Wainwright
University of Tulsa
,
Richard Chbeir
University of Pau & Pays Adour, France

Copyright © 2018 ACM.

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]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC 2018

Sponsor:

SIGAPP

SAC 2018: Symposium on Applied Computing

April 9 - 13, 2018

Pau, France

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
61
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jovanovic ASullivan A(2024)Mutation testing for temporal alloy models (extended version)Software and Systems Modeling10.1007/s10270-024-01220-xOnline publication date: 28-Oct-2024
https://doi.org/10.1007/s10270-024-01220-x
Sullivan A(2023)Integrating Testing into the Alloy Model Development Workflow2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)10.1109/MODELS58315.2023.00030(117-128)Online publication date: 1-Oct-2023
https://doi.org/10.1109/MODELS58315.2023.00030
Jovanovic ASullivan A(2023)Mutation Testing for Temporal Alloy Models2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)10.1109/MODELS58315.2023.00013(228-238)Online publication date: 1-Oct-2023
https://doi.org/10.1109/MODELS58315.2023.00013
Sullivan ABissyandé TKlein JBird CSarro F(2023)Live Programming for Finite Model FindersProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00016(1747-1752)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00016
Ringert JSullivan A(2023)Abstract Alloy InstancesFormal Methods10.1007/978-3-031-27481-7_21(364-382)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_21
Jovanovic ASullivan A(2022)REACH: Refining Alloy Scenarios by Size (Tools and Artifact Track)2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00031(229-238)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00031
Dini NZaeem RKhurshid SHung CHong JBechini ASong E(2021)Enhancing constraint-based repair of data structure errors that recur using memoizationProceedings of the 36th Annual ACM Symposium on Applied Computing10.1145/3412841.3442055(1823-1832)Online publication date: 22-Mar-2021
https://dl.acm.org/doi/10.1145/3412841.3442055
Sullivan A(2021)HawkEye: User-Guided Enumeration of Scenarios2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00064(569-578)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00064
Usman MWang WWang KYelen CDini NKhurshid S(2020)A study of learning likely data structure properties using machine learning modelsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00577-wOnline publication date: 7-Jun-2020
https://doi.org/10.1007/s10009-020-00577-w
Dini NYelen CGligoric MKhurshid S(2019)Extension-Aware Automated Testing Based on Imperative Predicates2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST.2019.00013(25-36)Online publication date: Apr-2019
https://doi.org/10.1109/ICST.2019.00013

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents