Objectives of talk • Introduce collaborative projects with (2008)
David Naumann, Paulo Borba, Ana Cavalcanti, Sampaio Federal, U. Pernambuco
and simulation
Abstract REFINE 2006 A Denotational Semantics for Circus (2008)
Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP. Previously, a denotational semantics has been given to Circus; however, as a shallow...
Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
Abstract. The increasing interest in the combination of different computational paradigms is well represented by Hoare & He in the Unifying Theories of Programming (UTP). In this paper, we...
Verification of Control Systems using Circus (2008)
The design of control systems is usually based on diagrammatic definitions of control laws. The independent use of Z and CSP to verify their implementations has been successful, even for very large...
Unifying classes and processes (2008)
Ana Cavalcanti, Augusto Sampaio, Jim Woodcock
Abstract. Previously, we presented Circus, an integration of Z, CSP, and Morgan’s refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for...
Testing for Refinement in CSP (2008)
Paris Sud, Ana Cavalcanti, Marie-claude Gaudel
Abstract. CSP is a well-established formalism for modelling and verification of concurrent reactive systems based on refinement. Consolidated denotational models and an effective tool have encouraged...
Refining Industrial Scale Systems in Circus (2008)
Ian East, Jeremy Martin, Peter Welch, David Duce, Mark Green (eds, Marcel Oliveira, ...
Abstract. Circus is a new notation that may be used to specify both data and behaviour aspects of a system, and has an associated refinement calculus. Although a
Abstract Refactoring by Transformation (2008)
Márcio Cornélio, Ana Cavalcanti, Augusto Sampaio
In this paper we present how refactoring of object-oriented programs can be accomplished by using refinement. Our approach is based on algebraic laws of an object-oriented language for refinement...
Cyber Rally: An Experience Of Democratic Use Of The Internet (2007)
Geber Ramalho Flvia, Geber Ramalho, Flvia Barros, Srgio Cavalcante, Ana Cavalcanti, Silvio Meira, ...
this paper can be a useful source of information to them.
Ana Cavalcanti, David A. Naumann
This extended abstract describes progress in an ongoing project on renement calculus for sequential Java. Predicate transformer semantics is being used to validate correctness-preserving...
Testing for Refinement in CSP (2007)
Cavalcanti, Ana, Gaudel, Marie-Claude
CSP is a well-established formalism for modelling and verifi- cation of concurrent reactive systems based on refinement. Consolidated denotational models and an effective tool have encouraged much...
List of Potential Supervisors (2007)
Neil Audsley, Jim Austin, Iain Bate, Ian Benest, Sam Braunstein, Alan Burns, ...
This document outlines some of the present research interests of most members of the Department who are in a position to supervise the research of students entering in October 2007. The sections are...
Automatic Translation from Circus to Java (2006)
Angela Freitas, Ana Cavalcanti
Abstract. Circus is a combination of Z and CSP that supports the development of state-rich reactive systems based on refinement. In this paper we present JCircus, a tool that automatically translates...
Pointers and records in the unifying theories of programming (2006)
Ana Cavalcanti, Will Harwood, Jim Woodcock
Abstract. We present a theory of pointers and records that provides a representation for objects and sharing in languages like Java and C++. Our approach to pointers is based on Paige’s entity...
Thread-Modular Verification is Cartesian Abstract Interpretation (2006)
Malkis, Alexander, Podelski, Andreas, Rybalchenko, Andrey, Barkaoui, Kamel, Cavalcanti, Ana, Cerone, Antonio
Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on...
Model checking Duration Calculus: a practical approach (2006)
Meyer, Roland, Faber, Johannes, Rybalchenko, Andrey, Barkaoui, Kamel, Cavalcanti, Ana, Cerone, Antonio
Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate....
Formal development of industrial-scale systems (2005)
Marcel Oliveira, Ana Cavalcanti, Jim Woodcock
Abstract. Circus is a new notation that may be used to specify both data and behavioural aspects of a system, and has an associated refinement calculus. In this work, we present rules to translate...
Operational Semantics for Model Checking Circus (2005)
Jim Woodcock, Ana Cavalcanti, Leonardo Freitas
Abstract. Circus is a combination of Z, CSP, and the refinement calculus, and is based on Hoare & He’s Unifying Theories of Programming. A model checker is being constructed for the language to...
Angelic Nondeterminism and Unifying Theories of Programming (2005)
Ana Cavalcanti, Jim Woodcock, Steve Dunne
Abstract. Hoare and He’s unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of...
Control law diagrams in Circus (2005)
Ana Cavalcanti, Phil Clayton, Malvern England
Abstract. Control diagrams are routinely used by engineers in the design of control systems. Yet, currently the formal verification of programs that implement the diagrams is a challenge. We present...
Angelic Nondeterminism and Unifying Theories of Programming (Extended Version (2004)
Ana Cavalcanti, Ana Cavalcanti, Jim Woodcock, Jim Woodcock
Abstract. Hoare and He have proposed unifying theories of programming (UTP): a model of alphabetised relations expressed as predicates, which provides support for program development in a number of...
Marcel Oliveira, Ana Cavalcanti
Abstract. Circus is a combination of Z, CSP, and Morgan’s refinement calculus; it has an associated refinement strategy that supports the development of reactive programs. In this work, we present...
Angelic Nondeterminism and Unifying Theories of Programming (Extended Version (2004)
Abstract. Hoare and He’s unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates, which supports development in several programming paradigms. The aim is...
Forward simulation for data refinement of classes (2002)
Ana Cavalcanti, David A. Naumann
Abstract. Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic...
JACK: A Framework for Process Algebra Implementation in Java (2002)
Leonardo Freitas, Augusto Sampaio, Ana Cavalcanti
The construction of concurrent programs is especially complex due mainly to the inherent non-determinism of their execution, which makes it difficult to repeat test scenarios. Process algebras have...
A Weakest Precondition Semantics for Refinement of Object-Oriented Programs (2000)
Ana Cavalcanti, David A. Naumann
We define a predicate-transformer semantics for an object-oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility...
A Weakest Precondition Semantics for an Object-oriented Language of Refinement (1999)
Ana Cavalcanti, David A. Naumann
We define a predicate-transformer semantics for an object-oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility...
A Weakest Precondition Semantics For Z (1997)
Ana Cavalcanti, Ana Cavalcanti, Jim Woodcock, Jim Woodcock
The lack of a method for developing programs from Z specifications is a difficulty widely recognised. In response to this problem, different approaches to the integration of Z with a refinement...
Procedures, Parameters, And Substitution In The Refinement Calculus (1997)
Ana Cavalcanti, Ana Cavalcanti, Augusto Sampaio, Augusto Sampaio, Jim Woodcock, Jim Woodcock
Morgan and Back have proposed different formalisations of procedures and parameters in the context of techniques of program development based on refinement. We investigate a surprising and intricate...