| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
A System for Compositional Verification of Asynchronous Objects
- 2012
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 77:12, s. 1289-1309
-
Journal article (peer-reviewed)abstract
- We present a semantics, calculus, and system for compositional verification of Creol, an object-oriented modelling language for concurrent distributed applications. The system is an instance of KeY, a framework for object oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, symbolic execution via explicit substitutions, and the taclet rule language, the presented system addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories specified by the interfaces of Creol units. Two example scenarios demonstrate the usage of the system. This article extends the conference paper of Ahrendt and Dylla (2009) with a denotational semantics of Creol and an assumption-commitment style semantics of the logic.
|
|
| 2. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
A Verification System for Distributed Objects with Asynchronous Method Calls
- 2009
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642103728 ; 5885, s. 387-406
-
Conference paper (peer-reviewed)abstract
- We present a verification system for Creol, an object-orientedmodeling language for concurrent distributed applications.The system is an instance of KeY, a framework for object oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, explicit substitutions, and the taclet rule language, the system presented in this paper addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories which describe the interfaces of Creol units. Two example scenarios demonstrate the usage of the system.
|
|
| 3. |
- Theobald, Martin, et al.
(author)
-
10 Years of Probabilistic Querying : What Next?
- 2013
-
In: Advances in Databases and Information Systems. - Berlin, Heidelberg : Springer. - 9783642406829 - 9783642406836 ; , s. 1-13
-
Conference paper (peer-reviewed)abstract
- Over the past decade, the two research areas of probabilistic databases and probabilistic programming have intensively studied the problem of making structured probabilistic inference scalable, but—so far—both areas developed almost independently of one another. While probabilistic databases have focused on describing tractable query classes based on the structure of query plans and data lineage, probabilistic programming has contributed sophisticated inference techniques based on knowledge compilation and lifted (first-order) inference. Both fields have developed their own variants of—both exact and approximate —top-k algorithms for query evaluation, and both investigate query optimization techniques known from SQL, Datalog, and Prolog, which all calls for a more intensive study of the commonalities and integration of the two fields. Moreover, we believe that natural-language processing and information extraction will remain a driving factor and in fact a longstanding challenge for developing expressive representation models which can be combined with structured probabilistic inference—also for the next decades to come.
|
|
