20 citations · 25 across the 10 of their papers we have counts for
10 papers
Model Repair via Symmetry
Paul Attie, William Cocke
The symmetry of a Kripke structure has been exploited to replace a model check of by a model check of the potentially smaller structure ob…
Operational Annotations: A new method for sequential program verification
Paul C Attie
I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of…
From Global Choreographies to Provably Correct and Efficient Distributed Implementations
Mohamad Jaber, Yliès Falcone, Paul Attie +2
We define a method to automatically synthesize provably-correct efficient distributed implementations from high-level global choreographies. A global choreography describes the exe…
Dynamic Input/Output Automata: a Formal and Compositional Model for Dynamic Systems
Paul C. Attie, Nancy A. Lynch
We present dynamic I/O automata (DIOA), a compositional model of dynamic systems. In DIOA, automata can be created and destroyed dynamically, as computation proceeds, and an automa…
Specification Construction Using Behaviours, Equivalences, and SMT Solvers
Paul C. Attie, Fadi A. Zaraket, Mohamad Noureddine +1
We propose a method to write and check a specification including quantifiers using behaviors, i.e., input-output pairs. Our method requires the following input from the user: (1) a…
Semantic Guidance and Feedback for the Construction of Specifications and Implementations
Paul C Attie, Fadi A Zaraket, Mohammad Fawaz +1
The problem of writing a specification which accurately reflects the intent of the developer has long been recognized as fundamental. We propose a method and a supporting tool to w…