| 34961. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A Semantics for Distributed Erlang
- 2005
-
Ingår i: Proceedings of the ACM SIGPLAN 2005 Erlang Workshop. - 1595930663
-
Konferensbidrag (refereegranskat)abstract
- We propose an extension to Fredlund's formal semantics for Erlang thatmodels the concept of nodes. The motivation is that there existsequences of events that can occur in practice, but are impossible todescribe using a single-node semantics, such as Fredlund's. Theconsequence is that some errors in distributed systems might not bedetected by model checkers based on Fredlund's original semantics, orby other single-node verification techniques such as testing. Ourextension is modest; it re-uses most of Fredlund's work but adds anextra layer at the top-level.
|
|
| 34962. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A supervisory control algorithm based on property-directed reachability
- 2017
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319703886 ; 10629 LNCS, s. 115-130
-
Konferensbidrag (refereegranskat)abstract
- We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for computer science has developed techniques and tools. In this paper, we attempt to marry the two by adapting PDR to the problem of controller synthesis. The resulting algorithm takes as input a transition system with forbidden states and uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution to the greater effort of formal supervisory controller synthesis and verification.
|
|
| 34963. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
An Operational Semantics for Weak PSL
- 2004
-
Ingår i: 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. ; 3312, s. 337-351
-
Tidskriftsartikel (refereegranskat)abstract
- Extending linear temporal logic by adding regular expressions increases its expressiveness. However, as for example, problems in recent versions of Accellera's Property Specification Language (PSL) as well as in OpenVera's ForSpec and other property languages show, it is a non-trivial task to give a formal denotational semantics with desirable properties to the resulting logic. In this paper, we argue that specifying an operational semantics may be helpful in guiding this work, and as a bonus leads to an implementation of the logic for free. We give a concrete operational semantics for Weak PSL, which is the safety property subset of PSL. We also propose a denotational semantics which we show to be equivalent to the operational one. This semantics is inspired by a new denotational semantics proposed in recent related work.
|
|
| 34964. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Automated Inference of Finite Unsatisfiability
- 2011
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:2, s. 111-132
-
Tidskriftsartikel (refereegranskat)abstract
- We present Infinox, an automated tool for analyzing first-order logic problems, aimed at showing finite unsatisfiability, i.e., the absence of models with finite domains. Finite satisfiability is not a decidable problem (only semi-decidable), which means that such a tool can never be complete. Nonetheless, our hope is that Infinox be a useful complement to finite model finders in practice. Infinox uses several different proof techniques for showing infinity of a set, each of which requires the identification of a function or a relation with particular properties. Infinox enumerates candidates to such functions and relations, and subsequently uses an automated theorem prover as a sub-procedure to try to prove the resulting proof obligations. We have evaluated Infinox on the relevant problems from the TPTP benchmark suite, and we are able to automatically show finite unsatisfiability for over 25% of these problems.
|
|
| 34965. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Automating Inductive Proofs using Theory Exploration
- 2013
-
Ingår i: 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. - 9783642385735 ; 7898, s. 392-406
-
Konferensbidrag (refereegranskat)abstract
- HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
|
|
| 34966. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Efficient Encodings of First-Order Horn Formulas in Equational Logic
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10900 LNAI, s. 388-404
-
Konferensbidrag (refereegranskat)abstract
- We present several translations from first-order Horn formulas to equational logic. The goal of these translations is to allow equational theorem provers to efficiently reason about non-equational problems. Using these translations we were able to solve 37 problems of rating 1.0 (i.e. which had not previously been automatically solved) from the TPTP.
|
|
| 34967. |
|
|
| 34968. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Expressive array constructs in an embedded GPU kernel programming language
- 2012
-
Ingår i: Conference Record of the Annual ACM Symposium on Principles of Programming Languages. - New York, NY, USA : ACM. - 0730-8566. - 9781450311175 ; , s. 21-30
-
Konferensbidrag (refereegranskat)abstract
- Graphics Processing Units (GPUs) are powerful computing devices that with the advent of CUDA/OpenCL are becomming useful for general purpose computations. Obsidian is an embedded domain specific language that generates CUDA kernels from functional descriptions. A symbolic array construction allows us to guarantee that intermediate arrays are fused away. However, the current array construction has some drawbacks; in particular, arrays cannot be combined efficiently. We add a new type of push arrays to the existing Obsidian system in order to solve this problem. The two array types complement each other, and enable the definition of combinators that both take apart and combine arrays, and that result in efficient generated code. This extension to Obsidian is demonstrated on a sequence of sorting kernels, with good results. The case study also illustrates the use of combinators for expressing the structure of parallel algorithms. The work presented is preliminary, and the combinators presented must be generalised. However, the raw speed of the generated kernels bodes well.
|
|
| 34969. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Finding Counter Examples in Induction Proofs
- 2008
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743.
-
Konferensbidrag (refereegranskat)abstract
- This paper addresses a problem arising in automated proof of invariants of transition systems, for example transition systems modelling distributed programs. Most of the time, the actual properties we want to prove are too weakto hold inductively, and auxiliary invariants need to be introduced. The problem is how to find these extra invariants. We propose a method where we find minimal counter examples to candidate invariants by means of automated random testing techniques. These counter examples can be inspected by a human user, and used to adapt the set of invariants at hand. We are able to find two different kinds of counter examples, either indicating (1) that the used invariants are too strong (a concrete trace of the system violates at least one of the invariants), or (2) that the used invariants are too weak (a concretetransition of the system does not maintain all invariants). We have developed and evaluated our method in the context of formally verifying an industrial-strength implementation of a fault-tolerant distributed leader election protocol.
|
|
| 34970. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Finding Race Conditions in Erlang with Quick Check and PULSE
- 2009
-
Ingår i: ICFP'09: Proceedings of the ACM SIGPLAN International Conference on Functional Programming. - New York, NY, USA : ACM. - 9781605583327 ; , s. 149-160
-
Konferensbidrag (refereegranskat)abstract
- We address the problem of testing and debugging concurrent, distributed Erlang applications. In concurrent programs, race conditions are a common class of bugs and are very hard to find in practice. Traditional unit testing is normally unable to help finding all race conditions, because their occurrence depends so much on timing. Therefore, race conditions are often found during system testing, where due to the vast amount of code under test, it is often hard to diagnose the error resulting from race conditions. We present three tools (Quick Check, PULSE, and a visualizer) that in combination can be used to test and debug concurrent programs in unit testing with a much better possibility of detecting race conditions. We evaluate our method on an industrial concurrent case study and illustrate how we find and analyze the race conditions.
|
|
