Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CONCUR
2011
Springer
9 years 10 months ago
Reasoning about Threads with Bounded Lock Chains
The problem of model checking threads interacting purely via the standard synchronization primitives is key for many concurrent program analyses, particularly dataflow analysis. U...
Vineet Kahlon
AAAI
2011
9 years 10 months ago
Preferred Explanations: Theory and Generation via Planning
In this paper we examine the general problem of generating preferred explanations for observed behavior with respect to a model of the behavior of a dynamical system. This problem...
Shirin Sohrabi, Jorge A. Baier, Sheila A. McIlrait...
POPL
2011
ACM
10 years 1 months ago
Making prophecies with decision predicates
We describe a new algorithm for proving temporal properties expressed in LTL of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be...
Byron Cook, Eric Koskinen
TII
2010
113views Education» more  TII 2010»
10 years 5 months ago
An Automated Framework for Formal Verification of Timed Continuous Petri Nets
In this paper, we develop an automated framework for formal verification of timed continuous Petri nets (ContPNs). Specifically, we consider two problems: (1) given an initial set ...
Marius Kloetzer, Cristian Mahulea, Calin Belta, Ma...
CDC
2010
IEEE
129views Control Systems» more  CDC 2010»
10 years 5 months ago
A symbolic approach to controlling piecewise affine systems
Abstract-- We present a computational framework for automatic synthesis of a feedback control strategy for a piecewise affine (PWA) system from a specification given as a Linear Te...
Jana Tumova, Boyan Yordanov, Calin Belta, Ivana Ce...
ICTAC
2009
Springer
10 years 8 months ago
A First-Order Policy Language for History-Based Transaction Monitoring
Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting,...
Andreas Bauer 0002, Rajeev Goré, Alwen Tiu
FM
2009
Springer
154views Formal Methods» more  FM 2009»
10 years 8 months ago
Specification and Verification of Web Applications in Rewriting Logic
Abstract. This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through icating protocol abstracting HTTP. The propo...
María Alpuente, Demis Ballis, Daniel Romero
CDC
2009
IEEE
132views Control Systems» more  CDC 2009»
10 years 8 months ago
Temporal logic control of discrete-time piecewise affine systems
Abstract-- We consider the problem of controlling a discretetime piecewise affine (PWA) system from a specification given as a Linear Temporal Logic (LTL) formula over linear predi...
Boyan Yordanov, Calin Belta
CDC
2009
IEEE
147views Control Systems» more  CDC 2009»
10 years 8 months ago
A probabilistic approach for control of a stochastic system from LTL specifications
We consider the problem of controlling a continuous-time linear stochastic system from a specification given as a Linear Temporal Logic (LTL) formula over a set of linear predicate...
Morteza Lahijanian, Sean B. Andersson, Calin Belta
WRLA
2010
10 years 9 months ago
The Linear Temporal Logic of Rewriting Maude Model Checker
Abstract. This paper presents the foundation, design, and implementation of the Linear Temporal Logic of Rewriting model checker as an extension of the Maude system. The Linear Tem...
Kyungmin Bae, José Meseguer
books