The maximal number of hits you can export is 250. When you want to export more records please use the 'Create feeds' function.

1.

Abdulla, Aziz

et al.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Delzanno, Giorgio

Rezine, Ahmed

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Holík, Lukás

Kaati, Lisa

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Krcal, Pavel

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Yi, Wang

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.

Universality of R-automata with value copying2009In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 239, p. 131-141Article in journal (Refereed)

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.

Parrow, Joachim

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.

We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt;rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.

Jonsson, Bengt

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.

Leucker, Martin

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.

Saksena, Mayank

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.

Insights to Angluin's Learning2005In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 118, p. 3-18Article in journal (Refereed)

Abstract [en]

Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied.

A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples.

We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.

Several symbolic notions of bisimilarity have been defined for the spi calculus and the applied pi calculus. In this paper, we treat a spi calculus with a general constructor-destructor message algebra, and define a symbolic bisimilarity that is both sound and complete with respect to its concrete counterpart.

Static Equivalence is Harder than Knowledge2006In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 154, no 3, p. 45-57Article in journal (Refereed)

Abstract [en]

There are two main ways of defining secrecy of cryptographic protocols. The first version checks if the adversary can learn the value of a secret parameter. In the second version, one checks if the adversary can notice any difference between protocol runs with different values of the secret parameter.

We give a new proof that when considering more complex equational theories than partially invertible functions, these two kinds of secrecy are not equally difficult to verify. More precisely, we identify a message language equipped with a convergent rewrite system such that after a completed protocol run, the first problem mentioned above (adversary knowledge) is decidable but the second problem (static equivalence) is not. The proof is by reduction of the ambiguity problem for context-free grammars.

A Chart Semantics for the Pi-Calculus2008In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 194, no 2, p. 3-29Article in journal (Refereed)

Abstract [en]

We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational semantics. A pi-chart is a finite directed acyclic graph recording a computation in the pi-calculus. Each node represents a process, and each edge either represents a computation step, or a message-passing interaction. Pi-charts enjoy a natural pictorial representation, akin to message sequence charts, in which vertical edges represent control flow and horizontal edges represent data flow based on message passing. A pi-chart represents a single computation starting from its top (the nodes with no ancestors) to its bottom (the nodes with no descendants). Unlike conventional reductions or transitions, the edges in a pi-chart induce ancestry and other causal relations on processes. We give both compositional and operational definitions of pi-charts, and illustrate the additional expressivity afforded by the chart semantics via a series of examples.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.

The GTO Toolset and Method2007In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 185, p. 77-91Article in journal (Refereed)

Abstract [en]

A suitable method supported by a toolset with a high degree of automation is a necessity for the successful employment of formal methods in industrial projects.

The GTO toolset and method have been developed, and successfully applied, to formal methods in safety-critical control applications related to railway signalling since the mid 1990s. The toolset and method support the entire formal methods process from writing and validating formal specifications, through modelling of the implementation to formal verification and analysis of verification results. One goal the toolset and method was to make formal methods more competitive by streamlining the process so that -- at least within an established application area -- individual verification tasks could be done in an "assembly line"-like fashion with minimum overhead.

In line with this goal, the toolset is intended for use with configurable systems, where a generic specification is applicable to a family of systems and adapted to a specific system using configuration data.

The functions carried out by the toolset include static checking and simulation of specifications, checking of configuration data, generation of implementation models from PLC program code or relay schematics, simulation of the implementation model, formal verification by refinement proof, and analysis of failed refinement proofs. Refinement proofs are automatically carried out by a satisfiability (SAT) solver of the user's choice, which is interfaced to the main tool.

We will outline the method and functions of the toolset as well as the formal notation -- a simple temporal predicate logic -- used by the toolset.

Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.

Expressiveness of Process Algebras2008In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 209, p. 173-186Article in journal (Refereed)

Abstract [en]

We examine ways to measure expressiveness of process algebras, and recapitulate and compare some related results from the literature.