Automated Predicate Abstraction for Real-Time Models (2009)
Badban, Bahareh, Leue, Stefan, Smaus, Jan-Georg
We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work...
Relaxation Refinement: A New Method to Generate Heuristic Functions (2009)
Jan-georg Smaus, Jörg Hoffmann
Abstract. In artificial intelligence, a relaxation of a problem is an overapproximation whose solution in every state of an explicit search provides a heuristic solution distance estimate. The...
Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL (2008)
Jörg Hoffmann, Jan-georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski
Abstract. We focus on checking safety properties in networks of extended timed automata, with the well-known UPPAAL system. We show how to use predicate abstraction, in the sense used in model...
Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL (2008)
Jörg Hoffmann, Jan-georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski
Abstract. We focus on checking safety properties in networks of extended timed automata, with the well-known UPPAAL system. We show how to use predicate abstraction, in the sense used in model...
• Formalizing Class Diagrams (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
• Embedding OCL into Isabelle/HOL • Conclusion
We briefly introduce two Isabelle/HOL applications, and one application of HOL Light: • Java bytecode verification; • floating-point arithmetic; • red-black trees. This is just to stimulate you...
Proof Environments for Formal Specification Languages (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Winter Term, Achim D. Brucker
Isabelle is not alone there are many successful theorem provers, e.g.: • Coq:
Verification-Integrated Falsification of Non-Deterministic Hybrid Systems (2006)
Stefan Ratschan, Jan-georg Smaus
Abstract This paper provides a method for coupling safety verification algo-rithms for non-deterministic (and, in general, non-linear) hybrid systems with the ability of finding concrete...
Verification-Integrated Falsification of Non-Deterministic Hybrid Systems (2006)
Ratschan, Stefan, Smaus, Jan-Georg, Cassandras, Christos, Giua, Alessandro, Seatzu, Carla, Zaytoon, Janan
• Formalizing Class Diagrams (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Well-founded Orders
◦ Z and Data-Refinement,
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Scons X Y
We are still looking at how the different parts of mathematics are encoded in the Isabelle/HOL library.
Higher-Order Logic (HOL) is: (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, David Basin
Higher-Order Logic (HOL) is: • an expressive foundation for mathematics: analysis, algebra,... computer science: program correctness, hardware verification,...
Termination of Simply Moded Logic Programs with Dynamic Scheduling (2004)
Bossi, Annalisa, Etalle, Sandro, Rossi, Sabina, Smaus, Jan-Georg
In logic programming, dynamic scheduling indicates the feature by means of which the choice of the atom to be selected at each resolution step is done at runtime and does not follow a fixed selection...
Termination of Simply Moded Logic Programs with Dynamic Scheduling (2004)
Annalisa Bossi, Sandro Etalle, Cwi Amsterdam, Jan-Georg Smaus, Sabina Rossi, Foscari Venezia, ...
this article, we provide a sucient and necessary criterion for termination of input consuming derivations of simply moded logic programs. The termination criterion we propose is based on a...
Termination of Simply Moded Logic Programs with Dynamic Scheduling (2003)
Bossi, Annalisa, Etalle, Sandro, Rossi, Sabina, Smaus, Jan-Georg
In logic programming, dynamic scheduling indicates the feature by means of which the choice of the atom to be selected at each resolution step is done at runtime and does not follow a fixed selection...
Bernd Krieg-brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, George Russell, ...
MMiSS Multi-Media Instruction in Safe and Secure Systems 4
MultiMedia Instruction in (2003)
Safe And Secure, Bernd Krieg-brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, ...
The aim of the MMiSS project is the construction of a multimedia Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure Systems....
M.: Multimedia instruction in safe and secure systems (2003)
Bernd Krieg-brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, Erica Melis, ...
Abstract. The aim of the MMiSS project is the construction of a multimedia Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure...
Classes of Terminating Logic Programs (2001)
Pedreschi, Dino, Ruggieri, Salvatore, Smaus, Jan-Georg
Termination of logic programs depends critically on the selection rule, i.e. the rule that determines which atom is selected in each resolution step. In this article, we classify programs (and...
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification (2001)
Analysis of (partial) groundness is an important application of abstract interpretation. There are several proposals for improving the precision of such an analysis by exploiting type information,...
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling (2001)
Bossi, Annalisa, Etalle, Sandro, Rossi, Sabina, Smaus, Jan-Georg
In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed selection rule...
2001. Semantics and termination of simplymoded logic programs with dynamic scheduling (2001)
Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-georg Smaus
Abstract. In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a xed selection...
2001. Semantics and termination of simplymoded logic programs with dynamic scheduling (2001)
Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-georg Smaus
Abstract. In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed...
Well-Typed Logic Programs Are not Wrong (2000)
Deransart, Pierre, Smaus, Jan-Georg
We consider prescriptive type systems for logic programs (as in Goedel or Mercury). In such systems, the typing is static, but it guarantees an operational property: if a program is "well-typed",...
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping (2000)
Smaus, Jan-Georg, Fages, Francois, Deransart, Pierre
We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the...
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping (2000)
Smaus, Jan-Georg, Fages, François, Deransart, Pierre
We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of \em subject reduction expresses the consistency of the type system...
Verifying Termination and Error-Freedom of Logic Programs with block Declarations (2000)
Smaus, Jan-Georg, Hill, Patricia M., King, Andy
We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present...
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping (2000)
Smaus, Jan-Georg, Fages, François, Deransart, Pierre
We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of \em subject reduction expresses the consistency of the type system...
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping (2000)
Smaus, Jan-Georg, Fages, François, Deransart, Pierre
We consider a general prescriptive type system with parametric polymorphism and subtyping for logic programs. The property of \em subject reduction expresses the consistency of the type system...
Mode Analysis Domains for Typed Logic Programs (2000)
Jan-Georg Smaus, Patricia M. Hill, Andy King
Precise mode information is important for compiler optimisations and in program development tools. Within the framework of abstract compilation, the precision of a mode analysis depends, in part, on...
Etalle, Sandro, Smaus, Jan-Georg
This volume contains the proceedings of the Workshop on Verification of Logic Programs, organised within the 1999 International Conference on Logic Programming. The workshop took place on December 1,...
Modes and types in logic programming. (1999)
Thesis (Ph. D.)--University of Kent at Canterbury, 1999.
Quotienting share for dependency analysis (1999)
Abstract. Def, the domain of denite Boolean functions, expresses (sure) dependencies between the program variables of, say, a constraint program. Share, on the other hand, captures the (possible)...
Domain Construction for Mode Analysis of Typed Logic Programs (1997)
Jan-Georg Smaus, Pat Hill, Andy King
There are many applications where precise mode analysis is required. However, within the framework of abstract interpretation, the precision of an analyser depends, in part, on the expressiveness of...