Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- articleFebruary 2009
Reactors: A data-oriented synchronous/asynchronous programming model for distributed applications
Theoretical Computer Science (TCSC), Volume 410, Issue 2-3Pages 168–201https://doi.org/10.1016/j.tcs.2008.09.052Our aim is to define the kernel of a simple and uniform programming model-the reactor model-which can serve as a foundation for building and evolving internet-scale programs. Such programs are characterized by collections of loosely-coupled distributed ...
- articleFebruary 2009
A shared-variable concurrency analysis of multi-threaded object-oriented programs
Theoretical Computer Science (TCSC), Volume 410, Issue 2-3Pages 128–141https://doi.org/10.1016/j.tcs.2008.09.024In this paper a proof outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. The main contribution is a generalization of the Owicki& Gries proof method for shared-variable concurrency to dynamic ...
- articleJuly 2008
Integration of a security type system into a program logic
Theoretical Computer Science (TCSC), Volume 402, Issue 2-3Pages 172–189https://doi.org/10.1016/j.tcs.2008.04.033Type systems and program logics are often thought to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring non-interference in a simple while-language can be expressed through ...
- articleAugust 2007
Model checking mobile stochastic logic
Theoretical Computer Science (TCSC), Volume 382, Issue 1Pages 42–70https://doi.org/10.1016/j.tcs.2007.05.008The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous work by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is to address key functional aspects of ...
- articleAugust 2007
CSL model checking algorithms for QBDs
Theoretical Computer Science (TCSC), Volume 382, Issue 1Pages 24–41https://doi.org/10.1016/j.tcs.2007.05.007We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of ...
-
- articleAugust 2007
Mixing logics and rewards for the component-oriented specification of performance measures
Theoretical Computer Science (TCSC), Volume 382, Issue 1Pages 3–23https://doi.org/10.1016/j.tcs.2007.05.006Formal notations for system performance modeling need to be equipped with suitable notations for specifying performance measures. These companion notations have been traditionally based on reward structures and, more recently, on temporal logics. In ...
- articleJuly 2007
The differential λμ-calculus
Theoretical Computer Science (TCSC), Volume 379, Issue 1-2Pages 166–209https://doi.org/10.1016/j.tcs.2007.02.028We define a differential @l@m-calculus which is an extension of both Parigot's @l@m-calculus and Ehrhard-Regnier's differential @l-calculus. We prove some basic properties of the system: reduction enjoys Church-Rosser and simply typed terms are strongly ...
- articleJuly 2007
Closure properties for the class of behavioral models
Theoretical Computer Science (TCSC), Volume 379, Issue 1-2Pages 53–83https://doi.org/10.1016/j.tcs.2007.01.024Hidden k-logics can be considered as the underlying logics of program specification. They constitute natural generalizations of k-deductive systems and encompass deductive systems as well as hidden equational logics and inequational logics. In our ...
- articleJuly 2007
Strong planning under uncertainty in domains with numerous but identical elements (a generic approach)
Theoretical Computer Science (TCSC), Volume 379, Issue 1-2Pages 84–119https://doi.org/10.1016/j.tcs.2007.01.022The typical AI problem is that of making a plan of the actions to be performed by a robot so that the robot could get into a set of final situations, if it started with a certain initial situation. The planning problem is known to be generally very ...
- articleApril 2007
Relational separation logic
Theoretical Computer Science (TCSC), Volume 375, Issue 1-3Pages 308–334https://doi.org/10.1016/j.tcs.2006.12.036In this paper, we present a Hoare-style logic for specifying and verifying how two pointer programs are related. Our logic lifts the main features of separation logic, from an assertion to a relation, and from a property about a single program to a ...
- articleApril 2007
Resources, concurrency, and local reasoning
Theoretical Computer Science (TCSC), Volume 375, Issue 1-3Pages 271–307https://doi.org/10.1016/j.tcs.2006.12.035In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.
- articleApril 2007
A semantics for concurrent separation logic
Theoretical Computer Science (TCSC), Volume 375, Issue 1-3Pages 227–270https://doi.org/10.1016/j.tcs.2006.12.034We present a trace semantics for a language of parallel programs which share access to mutable data. We introduce a resource-sensitive logic for partial correctness, based on a recent proposal of O'Hearn, adapting separation logic to the concurrent ...
- articleNovember 2006
Proof-carrying code from certified abstract interpretation and fixpoint compression
Theoretical Computer Science (TCSC), Volume 364, Issue 3Pages 273–291https://doi.org/10.1016/j.tcs.2006.08.012Proof-carrying code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's safety policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code ...
- articleFebruary 2006
On the expressive power of monadic least fixed point logic
Theoretical Computer Science (TCSC), Volume 350, Issue 2Pages 325–344https://doi.org/10.1016/j.tcs.2005.10.025Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper, we take a closer look at the expressive power of MLFP. Our results are: (1) MLFP ...
- articleJanuary 2006
Unifying logic, topology and learning in parametric logic
Theoretical Computer Science (TCSC), Volume 350, Issue 1Pages 103–124https://doi.org/10.1016/j.tcs.2005.10.018Many connections have been established between learning and logic, or learning and topology, or logic and topology. Still, the connections are not at the heart of these fields. Each of them is fairly independent of the others when attention is ...
- articleNovember 2005
A semantic framework for the abstract model checking of tccp programs
Theoretical Computer Science (TCSC), Volume 346, Issue 1Pages 58–95https://doi.org/10.1016/j.tcs.2005.08.009The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if ...
- articleNovember 2005
Quantitative μ-calculus and CTL defined over constraint semirings
Theoretical Computer Science (TCSC), Volume 346, Issue 1Pages 135–160https://doi.org/10.1016/j.tcs.2005.08.006Model checking and temporal logics are boolean. The answer to the model checking question does a system satisfy a property? is either true or false, and properties expressed in temporal logics are defined over boolean propositions. While this classic ...
- articleNovember 2005
Quantitative information in the tuple space coordination model
Theoretical Computer Science (TCSC), Volume 346, Issue 1Pages 28–57https://doi.org/10.1016/j.tcs.2005.08.004Tuple Spaces is a well-known coordination model at the basis of coordination languages such as Linda, JavaSpaces and TSpaces. Tuple spaces are flat and unstructured multisets of tuples that can be accessed via output, read, and input operations. We ...
- articleNovember 2005
A theory for execution-time derivation in real-time programs
Theoretical Computer Science (TCSC), Volume 346, Issue 1Pages 3–27https://doi.org/10.1016/j.tcs.2005.08.003We provide an abstract command language for real-time programs and outline how a partial correctness semantics can be used to compute execution times. The notions of a timed command, refinement of a timed command, the command traversal condition, and ...
- articleOctober 2005
A proof outline logic for object-oriented programming
Theoretical Computer Science (TCSC), Volume 343, Issue 3Pages 413–442https://doi.org/10.1016/j.tcs.2005.06.018This paper describes a proof outline logic that covers most typical object-oriented language constructs in the presence of inheritance and subtyping. The logic is based on a weakest precondition calculus for assignments and object allocation which takes ...