Search results for: Rajeev Alur

Items from 1 to 20 out of 133 results

chapter

Congruences for Visibly Pushdown Languages

Rajeev Alur, Viraj Kumar, P. Madhusudan, Mahesh Viswanathan

Lecture Notes in Computer Science > Automata, Languages and Programming > Automata and Formal Languages II > 1102-1114

We study congruences on words in order to characterize the class of visibly pushdown languages (Vpl), a subclass of context-free languages. For any language L, we define a natural congruence on words that resembles the syntactic congruence for regular languages, such that this congruence is of finite index if, and only if, L is a Vpl. We then study the problem of finding canonical minimal deterministic...

chapter

Branching Pushdown Tree Automata

Rajeev Alur, Swarat Chaudhuri

Lecture Notes in Computer Science > FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science > Contributed Papers – Track B > 393-404

We observe that pushdown tree automata (PTAs) known in the literature cannot express combinations of branching and pushdown properties. This is because a PTA processes the children of a tree node in possibly different control states but with identical stacks. We propose branching pushdown tree automata (BPTAs) as a solution. In a BPTA, a push-move views its matching pops as an unbounded, unordered...

chapter

Specification and Analysis of Network Resource Requirements of Control Systems

Gera Weiss, Sebastian Fischmeister, Madhukar Anand, Rajeev Alur

Lecture Notes in Computer Science > Hybrid Systems: Computation and Control > Regular Papers > 381-395

We focus on spatially distributed control systems in which measurement and actuation data is sent via a bus shared with other applications. An approach is proposed for specifying and implementing dynamic scheduling policies for the bus with performance guarantees. Specifically, we propose an automata-based scheduler which we automatically generate from a model of the controlled plant and the controller...

chapter

A Temporal Logic of Nested Calls and Returns

Rajeev Alur, Kousha Etessami, P. Madhusudan

Lecture Notes in Computer Science > Tools and Algorithms for the Construction and Analysis of Systems > Temporal Logic > 467-481

Model checking of linear temporal logic (LTL) specifications with respect to pushdown systems has been shown to be a useful tool for analysis of programs with potentially recursive procedures. LTL, however, can specify only regular properties, and properties such as correctness of procedures with respect to pre and post conditions, that require matching of calls and returns, are not regular. We introduce...

chapter

Model Checking on Trees with Path Equivalences

Rajeev Alur, Pavol Černý, Swarat Chaudhuri

Lecture Notes in Computer Science > Tools and Algorithms for the Construction and Analysis of Systems > Model Checking > 664-678

For specifying and verifying branching-time requirements, a reactive system is traditionally modeled as a labeled tree, where a path in the tree encodes a possible execution of the system. We propose to enrich such tree models with “jump-edges” that capture observational indistinguishability: for an agent a, an a-labeled edge is added between two nodes if the observable behaviors of the agent a along...

chapter

Deciding global partial-order properties

Rajeev Alur, Ken McMillan, Doron Peled

Lecture Notes in Computer Science > Automata, Languages and Programming > 41-52

Model checking of asynchronous systems is traditionally based on the interleaving model, where an execution is modeled by a total order between events. Recently, the use of partial order semantics that allows independent events of concurrent processes to be unordered is becoming popular. Temporal logics that are interpreted over partial orders allow specifications relating global snapshots, and permit...

book

Embedded Software

Rajeev Alur, Insup Lee

Lecture Notes in Computer Science

This book constitutes the refereed proceedings of the Third International Conference on Embedded Software, EMSOFT 2003, held in Philadelphia, PA, USA in October 2003. The 20 revised full papers presented together with three invited papers were carefully reviewed and selected from 60 submissions. All current topics in embedded software are addressed: formal methods and model-based development, middleware...

chapter

Efficient Formal Verification of Hierarchical Descriptions

Rajeev Alur

Lecture Notes in Computer Science > Foundations of Software Technology and Theoretical Computer Science > Invited Talk 4 > 269-269

Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of hierarchical (nested) systems, i.e. finite state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies and is available in several commercial modeling tools. The straightforward way...

chapter

Algorithmic Analysis of Array-Accessing Programs

Rajeev Alur, Pavol Černý, Scott Weinstein

Lecture Notes in Computer Science > Computer Science Logic > Contributed Papers > 86-101

For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially...

chapter

Heuristics for Hierarchical Partitioning with Application to Model Checking

M. Oliver Möller, Rajeev Alur

Lecture Notes in Computer Science > Correct Hardware Design and Verification Methods > Model Checking 1 > 71-85

Given a collection of connected components, it is often desired to cluster together parts of strong correspondence, yielding a hierarchical structure. We address the automation of this process and apply heuristics to battle the combinatorial and computational complexity. We define a cost function that captures the quality of a structure relative to the connections and favors shallow structures...

chapter

Nondeterministic Streaming String Transducers

Rajeev Alur, Jyotirmoy V. Deshmukh

Lecture Notes in Computer Science > Automata, Languages and Programming > Invited Lectures > 1-20

We introduce nondeterministic streaming string transducers (nssts) – a new computational model that can implement MSO-definable relations between strings. An nsst makes a single left-to-right pass on the input string and uses a finite set of string variables to compute the output. In each step, it reads one input symbol, and updates its string variables in parallel with a copyless assignment. We show...

chapter

Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition

Wonhong Nam, Rajeev Alur

Lecture Notes in Computer Science > Automated Technology for Verification and Analysis > Regular Papers > 170-185

Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on the assume-guarantee reasoning principles, and requires decomposing the system into components as well as identifying adequate environment assumptions for components. One recent approach to automatic derivation of adequate assumptions...

chapter

Automated Analysis of Java Methods for Confidentiality

Pavol Černý, Rajeev Alur

Lecture Notes in Computer Science > Computer Aided Verification > Regular Papers > 173-187

We address the problem of analyzing programs such as J2ME midlets for mobile devices, where a central correctness requirement concerns confidentiality of data that the user wants to keep secret. Existing software model checking tools analyze individual program executions, and are not applicable to checking confidentiality properties that require reasoning about equivalence among executions. We develop...

chapter

Playing Games with Boxes and Diamonds

Rajeev Alur, Salvatore Torre, P. Madhusudan

Lecture Notes in Computer Science > CONCUR 2003 - Concurrency Theory > Games > 128-143

Deciding infinite two-player games on finite graphs with the winning condition specified by a linear temporal logic (Ltl) formula, is known to be 2Exptime-complete. The previously known hardness proofs encode Turing machine computations using the next and/or until operators. Furthermore, in the case of model checking, disallowing next and until, and retaining only the always and eventually operators,...

chapter

Compression of Partially Ordered Strings

Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, Sudipto Guha, more

Lecture Notes in Computer Science > CONCUR 2003 - Concurrency Theory > Partial Orders and Asynchronous Systems > 42-56

We introduce the problem of compressing partially ordered strings: given string σεΣ^* and a binary independence relation I over Σ, how can we compactly represent an input if the decompressor is allowed to reconstruct any string that can be obtained from σ by repeatedly swapping adjacent independent symbols? Such partially ordered strings are also known as Mazurkiewicz traces, and naturally model executions...

chapter

“Next” Heuristic for On-the-Fly Model Checking

Rajeev Alur, Bow-Yaw Wang

Lecture Notes in Computer Science > CONCUR’99 Concurrency Theory > Accepted Papers > 98-113

We present a new heuristic for on-the-fly enumerative invariant verification. The heuristic is based on a construct for temporal scaling, called next, that compresses a sequence of transitions leading to a given target set into a single metatransition. First, we give an on-the-fly algorithm to search a process expression built using the constructs of hiding, parallel composition, and temporal scaling...

chapter

Workshop 2+8 Performance evaluation and prediction

Allen D. Malony, Rajeev Alur

Lecture Notes in Computer Science > Euro-Par’98 Parallel Processing > 191-192

chapter

Communicating Hierarchical State Machines

Rajeev Alur, Sampath Kannan, Mihalis Yannakakis

Lecture Notes in Computer Science > Automata, Languages and Programming > Contributed Papers > 169-178

Hierarchical state machines are finite state machines whose states themselves can be other machines. In spite of their popularity in many modeling tools for software design, very little is known concerning their complexity and expressiveness. In this paper, we study these questions for hierarchical state machines as well as for communicating hierarchical state machines, that is, finite state...

chapter

Trends and Challenges in Algorithmic Software Verification

Rajeev Alur

Lecture Notes in Computer Science > Verified Software: Theories, Tools, Experiments > Design, Analysis and Tools > 245-250

Recent years have witnessed remarkable progress in principles and tools for automated software verification. In this position paper, I briefly discuss the relevant projects in my group, and outline some near-term challenges for the community as concrete milestones for measuring progress.

chapter

Automata for modeling real-time systems

Rajeev Alur, David Dill

Lecture Notes in Computer Science > Automata, Languages and Programming > 322-335

To model the behavior of finite-state asynchronous real-time systems we propose the notion of timed Büchi automata (TBA). TBAs are Büchi automata coupled with a mechanism to express constant bounds on the timing delays between system events. These automata accept languages of timed traces, traces in which each event has an associated real-valued time of occurrence. We show that the class of...

Publication date

Set your own date range

Content availability

Available (127)
None (6)

Publication type

book (103)
article (30)

Keywords

FORMAL VERIFICATION (6)
MODEL CHECKING (6)
HYBRID SYSTEMS (5)
COMPUTATIONAL MODELING (3)
CONCURRENCY (3)
FORMAL METHODS (3)
REAL-TIME SYSTEMS (3)
REGISTERS (3)
SOFTWARE VERIFICATION (3)
TIMED AUTOMATA (3)
ASSUME-GUARANTEE REASONING (2)
AUTOMATA (2)
AUTOMATA THEORY (2)
AUTOMATIC VERIFICATION (2)
CAV AWARD (2)
COMPUTER-AIDED VERIFICATION (2)
COMPUTERS (2)
CONTROL SYSTEMS (2)
FORMAL LANGUAGES (2)
MONADIC SECOND-ORDER LOGIC (2)
SOFTWARE (2)
STREAMING STRING TRANSDUCERS (2)
SYMBOLIC MODEL CHECKING (2)
TRANSDUCERS (2)
VERIFICATION (2)
$\OMEGA$-REGULAR TRANSFORMATIONS (1)
ADDITIVES (1)
AWARDS ACTIVITIES (1)
BLACKWELL OPTIMALITY (1)
BOUNDED MODEL CHECKING (1)
CARA SYSTEM (1)
CEGAR (1)
COMMUTATION (1)
COMPOSITIONAL ANALYSIS (1)
COMPOSITIONAL MODEL CHECKING (1)
COMPOSITIONAL SEMANTICS (1)
COMPOSITIONAL VERIFICATION (1)
COMPOSITIONALITY (1)
COMPUTER LANGUAGES (1)
COMPUTER SCIENCE (1)
CONCURRENCY MODELING (1)
CONTEXT (1)
COST ACCOUNTING (1)
COST FUNCTION (1)
COUNTEREXAMPLE ANALYSIS (1)
COUNTEREXAMPLE-DRIVEN ABSTRACTION REFINEMENT (1)
CYBER-PHYSICAL SYSTEMS (1)
DATA MODELS (1)
DURATION PROPERTIES (1)
EDUCATIONAL INSTITUTIONS (1)
EMBEDDED SOFTWARE (1)
FINITE-STATE MACHINES (1)
GAMES (1)
GAMES IN VERIFICATION (1)
GRAMMAR (1)
HARDWARE (1)
HYPERGRAPH PARTITIONING (1)
IMPLANTABLE PACEMAKER (1)
INFORMATION SCIENCE (1)
INSTRUCTION SETS (1)
INTERPOLATION (1)
KEY WORDS: REAL-TIME SYSTEMS – REAL-TIME PROGRAMS – CLOCK VARIABLES – SEMANTICS AND VERIFICATION (1)
LITMUS TESTS (1)
MEDICAL DEVICES (1)
MEMORY CONSISTENCY MODELS (1)
MEMORY MANAGEMENT (1)
MESSAGE SEQUENCE CHARTS (1)
MODEL ABSTRACTION AND REFINEMENT (1)
MODEL REFINEMENT (1)
MODEL-BASED DESIGN (1)
MODEL-CHECKING (1)
MODELING OF REACTIVE SYSTEMS (1)
MULTI-HOP SENSOR AND ACTUATOR NETWORKS (1)
NETWORKED CONTROL (1)
OMEGA-REGULAR TRANSFORMATIONS (1)
OPTIMAL REACHABILITY (1)
OPTIMIZATION (1)
PARTIAL ORDER LOGICS (1)
POLYHEDRAL DYNAMICS (1)
PREDICATE ABSTRACTION (1)
PROBABILISTIC SYSTEMS (1)
PROGRAM CORRECTNESS (1)
PROGRAM VERIFICATION (1)
PUSHDOWN SYSTEMS (1)
QBF SOLVING (1)
QUANTITATIVE ANALYSIS (1)
REACHABILITY ANALYSIS (1)
REAL TIME (1)
REAL-TIME (1)
REAL-TIME SCHEDULING (1)
REAL-TIME SYSTEMS REAL-TIME PROGRAMS CLOCK VARIABLES SEMANTICS AND VERIFICATION (1)
REGULAR LANGUAGE LEARNING (1)
REQUIREMENTS FORMALIZATION (1)
SAFETY-CRITICAL SYSTEMS (1)
SCHEDULES (1)
SEMANTICS (1)
SENSORS (1)
SHARED MEMORY ALGORITHMS MUTUAL EXCLUSION CONSENSUS TIMING BASED MODEL CONTENTION FREE COMPLEXITY (1)
SOFTWARE SPECIFICATION (1)
SPACE EXPLORATION (1)
more

Data set

Springer (108)
Elsevier (13)
ieee (12)

INFONA - science communication portal

Search results for: Rajeev Alur

Congruences for Visibly Pushdown Languages

Branching Pushdown Tree Automata

Specification and Analysis of Network Resource Requirements of Control Systems

A Temporal Logic of Nested Calls and Returns

Model Checking on Trees with Path Equivalences

Deciding global partial-order properties

Embedded Software

Efficient Formal Verification of Hierarchical Descriptions

Algorithmic Analysis of Array-Accessing Programs

Heuristics for Hierarchical Partitioning with Application to Model Checking

Nondeterministic Streaming String Transducers

Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition

Automated Analysis of Java Methods for Confidentiality

Playing Games with Boxes and Diamonds

Compression of Partially Ordered Strings

“Next” Heuristic for On-the-Fly Model Checking

Workshop 2+8 Performance evaluation and prediction

Communicating Hierarchical State Machines

Trends and Challenges in Algorithmic Software Verification

Automata for modeling real-time systems

Filter options

Publication date

Content availability

Publication type

Keywords

Data set

Journal

INFONA - science communication portal

Search results for: Rajeev Alur

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Content availability

Publication type

Keywords

Data set

Journal

Reporting an error / abuse

Sending the report failed

Accessibility options