| 1. |
|
|
| 2. |
- Artho, Cyrille, et al.
(författare)
-
Model-based Testing of Stateful APIs with Modbat
- 2015
-
Ingår i: Proc. 30th Int. Conf. on Automated Software Engineering (ASE 2015). - : IEEE conference proceedings. ; , s. 858-863
-
Konferensbidrag (refereegranskat)abstract
- Modbat makes testing easier by providing a user-friendly modeling language to describe the behavior of systems, from such a model, test cases are generated and executed. Modbat's domain-specific language is based on Scala, its features include probabilistic and non-deterministic transitions, component models with inheritance, and exceptions. We demonstrate the versatility of Modbat by finding a confirmed defect in the currently latest version of Java, and by testing SAT solvers.
|
|
| 3. |
|
|
| 4. |
- Oetsch, Johannes, et al.
(författare)
-
A tool for advanced correspondence checking in answer-set programming : Preliminary experimental results
- 2006
-
Ingår i: Proceedings of the 20th Workshop on Logic Programming, WLP 2006. - : Institut fur Informationssysteme Arbeitsbereich. ; , s. 200-205
-
Konferensbidrag (refereegranskat)abstract
- In recent work, a general framework for specifying program correspondences under the answer-set semantics has been defined. The framework allows to define different notions of equivalence, including the well-known notions of strong and uniform equivalence, as well as refined equivalence notions based on the projection of answer sets, where not all parts of an answer set are of relevance (like, e.g., removal of auxiliary letters). In the general case, deciding the correspondence of two programs lies on the fourth level of the polynomial hierarchy and therefore this task can (presumably) not be efficiently reduced to answer-set programming. In this paper, we give an overview about an implementation to compute program correspondences in this general framework. The system, called eqcheck, relies on linear-time constructible reductions to quantified propositional logic using extant solvers for the latter language as back-end inference engines. We provide some preliminary performance evaluation, which shed light on some crucial design issues.
|
|
| 5. |
- Oetsch, Johannes, et al.
(författare)
-
A tool for advanced correspondence checking in answer-set programming
- 2006
-
Ingår i: Proceedings of the 11th Workshop on Nonmonotonic Reasoning. - Clausthal-Zellerfeld : Clausthal University of Technology. ; , s. 20-28
-
Konferensbidrag (refereegranskat)abstract
- In previous work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework allows to define different notions of equivalence, including well-known notions like strong equivalence as well as refined ones based on the projection of answer sets, where not all parts of an answer set are of relevance (like, e.g., removal of auxiliary letters). In the general case, deciding the correspondence of two programs lies on the fourth level of the polynomial hierarchy and therefore this task can (presumably) not be efficiently reduced to answer-set programming. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called cc⊤, relies on linear-time constructible reductions to quantified propositional logic using extant solvers for the latter language as back-end inference engines. We provide some preliminary performance evaluation which shed light on some crucial design issues.
|
|
| 6. |
- Oetsch, Johannes, et al.
(författare)
-
An Extension of the System cc⊤ for Testing Relativised Uniform Equivalence under Answer-Set Projection
- 2007
-
Ingår i: Proceedings of the 16th International Conference on Computing (CIC 2007).
-
Konferensbidrag (refereegranskat)abstract
- The system cc⊤ is a tool for testing correspondence between nonmonotonic logic programs under the answer-set semantics with respect to different refined notions of program correspondence. The basic architecture of cc⊤ is to reduce a given correspondence problem into the satisfiability problem for quantified propositional logic and to employ off-the-shelf solvers for the latter language as backend inference engines. In a previous incarnation of cc⊤, the system was designed to test correspondence between logic programs based on relativised strong equivalence under answer-set projection. Such a setting generalises the usual notion of strong equivalence by taking the alphabet of the context programs as well as the projection of the compared answer sets to a set of designated output atoms into account. In this paper, we describe an extension of cc⊤ for testing similarly parameterised correspondence problems but generalising uniform equivalence, which have recently been introduced in previous work. Besides reviewing the formal underpinnings of the new component of cc⊤, we discuss an alternative encoding as well as optimisations for special problem classes. Furthermore, we give a preliminary performance evaluation of the new component.
|
|
| 7. |
- Oetsch, Johannes, et al.
(författare)
-
Beyond Uniform Equivalence between Answer-set Programs
- 2021
-
Ingår i: ACM Transactions on Computational Logic. - : ACM Digital Library. - 1529-3785 .- 1557-945X. ; 22:1
-
Tidskriftsartikel (refereegranskat)abstract
- This article deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of considerable interest, because such notions form the basis for program verification and are useful for program optimisation, debugging, and modular programming. In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is uniform equivalence, which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this article, we study a family of more fine-grained versions of uniform equivalence, viz. relativised uniform equivalence with projection, which extends standard uniform equivalence in terms of two additional parameters: One for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for projecting answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms, which is important for practical programming aspects. We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse their computational complexity. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. Therefore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to quantified Boolean formulas (QBFs) are feasible. Indeed, we provide efficient (in fact, linear-time constructible) reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system cc ĝŠCurrency sign, for deciding correspondence problems by using off-the-shelf QBF solvers. We discuss an application of cc ĝŠCurrency sign for verifying the correctness of solutions by students drawn from a laboratory course on logic programming and knowledge representation at the Technische Universität Wien, employing relativised uniform equivalence with projection as the underlying program correspondence notion.
|
|
| 8. |
- Oetsch, Johannes, et al.
(författare)
-
Cc ⊤ : A tool for checking advanced correspondence problems in answer-set programming
- 2006
-
Ingår i: Proceedings - 15th International Conference on Computing, CIC 2006. - : IEEE. - 0769527086 - 9780769527086 ; , s. 3-10
-
Konferensbidrag (refereegranskat)abstract
- In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework allows to define different notions of equivalence, including well-known notions like strong equivalence as well as refined ones based on the projection of answer sets, where not all parts of an answer set are of relevance. In this paper, we describe a system, called cc ⊤, to verify program correspondences in this general framework, relying on linear-time constructible reductions to quantified propositional logic using extant solvers for the latter language as back-end inference engines. We provide a preliminary performance evaluation which sheds light on some crucial design issues.
|
|
| 9. |
- Oetsch, Johannes, et al.
(författare)
-
Cc Τ on stage : Generalised uniform equivalence testing for verifying student assignment solutions
- 2009
-
Ingår i: Logic Programming and Nonmonotonic Reasoning. - Berlin, Heidelberg : Springer. - 3642042376 - 9783642042379 ; , s. 382-395
-
Konferensbidrag (refereegranskat)abstract
- The tool cc Τ is an implementation for testing various parameterised notions of program correspondence between logic programs under the answer-set semantics, based on reductions to quantified propositional logic. One such notion is relativised uniform equivalence with projection, which extends standard uniform equivalence via two additional parameters: one for specifying the input alphabet and one for specifying the output alphabet. In particular, the latter parameter is used for projecting answer sets to the set of designated output atoms, i.e. ignoring auxiliary atoms during answer-set comparison. In this paper, we discuss an application of cc Τ for verifying the correctness of students' solutions drawn from a laboratory course on logic programming, employing relativised uniform equivalence with projection as the underlying program correspondence notion. We complement our investigation by discussing a performance evaluation of cc Τ, showing that discriminating among different back-end solvers for quantified propositional logic is a crucial issue towards optimal performance.
|
|
| 10. |
- Oetsch, Johannes, et al.
(författare)
-
ccT : A correspondence-checking tool for logic programs under the answer-set semantics
- 2006
-
Ingår i: Logics in Artificial Intelligence. - Berlin : Springer. - 354039625X - 9783540396253 ; , s. 502-505
-
Konferensbidrag (refereegranskat)abstract
- In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called ccT, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines.
|
|
