We give equational axioms for the least fixed point operation and point out applications to automata, languages, and concurrency.
read moreDynamic Delta Modeling
Software Product Lines (SPL) are sets of software products, which differ only by which features they support. Abstract Delta Modeling (ADM) shows how to organize a code-base in a natural way by structured reuse. Then, given a feature configuration (a set of desired features), we can mechanically generate any product …
read moreHow far can Enterprise Modeling for Banking be supported by Graph Transformation?
This talk presents results coming out of an ongoing research project between Credit Suisse Luxembourg and the TU Berlin. It presents an approach that shows good potential to address security, risk and compliance issues the bank has in its daily business by the use of integrated organizational models build up …
read moreAbstract Object Creation in First Order Dynamic Logic: State of the Art in Key
We present the state of the art in the KeY Java theorem prover, which is based on a first-order object-oriented dynamic logic.This assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from aspecific implementation of object creation. Objects which …
read moreHierarchical and modular reasoning in complex theories and applications to verification
A long term goal of the research in computer science is the analysis and verification of complex systems (these can for instance be programs, reactive or hybrid systems, large databases). In many cases, correctness proofs for such systems can be reduced to reasoning in complex logical theories (for instance, combinations …
read moreSimilarity-based Web Service Discovery through Soft Constraint Satisfaction Problems
In this talk, we focus on the discovery process of Web Services (WSs) by basing the search on the similarities among the service requirements, in order to cope with over-constrained queries or to find satisfactory alternatives for user requirements. This discovery process needs to involve the so-called Soft Constraint Satisfaction …
read moreModularizing and Specifying Protocols among Threads
We identify two problems with general-purpose programming languages: (i) they do not enforce separation of computations and protocols and (ii) they do not provide an appropriate level of abstraction to implement protocols. To mend these deficiencies, we argue for the use of domain-specific languages (DSL). A concrete instance then demonstrates …
read moreProgramming and Deployment of Active Objects with Application-Level Scheduling
We extend and implement a modeling language based on concurrent active objects with application-level scheduling policies. The language allows a programmer to assign priorities at the application level, for example, to method definitions and method invocations, and assign corresponding policies to the individual active objects for scheduling the messages. Thus …
read moreAbstract Compilation for Precise Type Analysis of Object-Oriented Languages
Abstract compilation is a novel approach to static type analysis aiming to reconcile types, symbolic execution and compiler technology: analyzing an expression consists in solving the goal generated from its compilation w.r.t. the coinductive model of the constraint logic program generated from the compilation of the source program …
read moreReactive Turing Machines
We propose reactive Turing machines (RTMs), extending classical Turing machines with a process-theoretical notion of interaction, and use it to define a notion of executable transition system. We show that every computable transition system with a bounded branching degree is simulated modulo divergence-preserving branching bisimilarity by an RTM, and that …
read more