ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Digital Library logoTake a look at the new version of this page: [ beta version ]. Tell us what you think.
Specification and verification of concurrent systems in CESAR
Source Lecture Notes In Computer Science; Vol. 137 archive
Proceedings of the 5th Colloquium on International Symposium on Programming table of contents
Pages: 337 - 351  
Year of Publication: 1982
ISBN:3-540-11494-7
Authors
Jean-Pierre Queille
Joseph Sifakis
Publisher
Springer-Verlag  London, UK
Bibliometrics
Downloads (6 Weeks): n/a,   Downloads (12 Months): n/a,   Citation Count: 107
Additional Information:

cited by   collaborative colleagues  

Tools and Actions: Review this Article  

CITED BY  107
Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997
Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996
Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland
Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000
R. P. Kurshan, The complexity of verification, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.365-371, May 23-25, 1994, Montreal, Quebec, Canada
Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.124-133, March 1998
E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986
P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany
Rance Cleaveland , Scott A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys (CSUR), v.28 n.4, p.607-625, Dec. 1996
Joseph Y. Halpern , Lenore D. Zuck, A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols, Journal of the ACM (JACM), v.39 n.3, p.449-478, July 1992
E M Clarke , O Grumberg , M C Browne, Reasoning about networks with many identical finite-state processes, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.240-248, August 11-13, 1986, Calgary, Alberta, Canada
Rajeev Alur , Lalita Jategaonkar Jagadeesan , Joseph J. Kott , James E. Von Olnhausen, Model-checking of real-time systems: a telecommunications application: experience report, Proceedings of the 19th international conference on Software engineering, p.514-524, May 17-23, 1997, Boston, Massachusetts, United States
Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
Orna Kupferman , Moshe Y. Vardi, An automata-theoretic approach to modular model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.87-128, Jan. 2000
David Lesens , Nicolas Halbwachs , Pascal Raymond, Automatic verification of parameterized linear networks of processes, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-357, January 15-17, 1997, Paris, France
Pierre Wolper, Constructing automata from temporal logic formulas: a tutorial, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.273-303, May 2001
Guoping Jia , Susanne Graf, Verification experiments on the MASCARA protocol, Proceedings of the 8th international SPIN workshop on Model checking of software, p.123-142, May 2001, Toronto, Ontario, Canada
Stephen Edwards , Luciano Lavagno , Edward A. Lee , Alberto Sangiovanni-Vincentelli, Design of embedded systems: formal models, validation, and synthesis, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997
Ahmed Bouajjani , Rachid Echahed , Peter Habermehl, Verifying infinite state processes with sequential and parallel composition, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-106, January 23-25, 1995, San Francisco, California, United States
Christophe Ratel , Nicolas Halbwachs , Pascal Raymond, Programming and verifying critical systems by means of the synchronous data-flow language LUSTRE, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.112-119, Dec. 1991
Paulo J. F. Carreira , Miguel E. F. Costa, Automatically verifying an object-oriented specification of the steam-boiler system, Science of Computer Programming, v.46 n.3, p.197-217, March 2003
C. R. Ramakrishnan , R. Sekar, Model-based analysis of configuration vulnerabilities, Journal of Computer Security, v.10 n.1-2, p.189-209, 2002
Michael Baldamus , Klaus Schneider, The BDD space complexity of different forms of concurrency, Fundamenta Informaticae, v.50 n.2, p.111-133, April 2002
Michael Dekhtyar , Alexander Dikovsky , Mars Valiev, On feasible cases of checking multi-agent systems behavior, Theoretical Computer Science, v.303 n.1, p.63-81, 28 June 2003
Amy P. Felty , Kedar S. Namjoshi, Feature specification and automated conflict detection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.1, p.3-27, January 2003
William N. Robinson , Suzanne D. Pawlowski , Vecheslav Volkov, Requirements interaction management, ACM Computing Surveys (CSUR), v.35 n.2, p.132-190, June 2003
Fei Xie , James C. Browne, Verified systems by composition from verified components, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
Panagiotis Manolios , Richard Trefler, A lattice-theoretic characterization of safety and liveness, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.325-333, July 13-16, 2003, Boston, Massachusetts
Greg Dennis , Robert Seater , Derek Rayside , Daniel Jackson, Automating commutativity analysis at the design level, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Henny B. Sipma , Tomás E. Uribe , Zohar Manna, Deductive Model Checking, Formal Methods in System Design, v.15 n.1, p.49-74, July 1999
Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.175-188, Nov. 1998
Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
Shoham Ben-David , Cindy Eisner , Daniel Geist , Yaron Wolfsthal, Model Checking at IBM, Formal Methods in System Design, v.22 n.2, p.101-108, March 2003
Shaz Qadeer, Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking, IEEE Transactions on Parallel and Distributed Systems, v.14 n.8, p.730-741, August 2003
Dimitra Giannakopoulou , Jeff Magee, Fluent model checking for event-based systems, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE, IEEE Transactions on Software Engineering, v.18 n.9, p.785-793, September 1992
David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
Parosh Aziz Abdulla , Bengt Jonsson, Model checking of systems with many identical timed processes, Theoretical Computer Science, v.290 n.1, p.241-264, 1 January 2003
Saddek Bensalem , Yassine Lakhnech, Automatic Generation of Invariants, Formal Methods in System Design, v.15 n.1, p.75-92, July 1999
Pao-Ann Hsiung , Shang-Wei Lin , Chih-Hao Tseng , Trong-Yen Lee , Jih-Ming Fu , Win-Bin See, VERTAF: An Application Framework for the Design and Verification of Embedded Real-Time Software, IEEE Transactions on Software Engineering, v.30 n.10, p.656-674, October 2004
Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
Ruggero Lanotte , Andrea Maggiolo-Schettini , Simone Tini, Information flow in hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.3 n.4, p.760-799, November 2004
Thomas A. Henzinger , Orna Kupferman , Shaz Qadeer, From Pre-Historic to Post-Modern Symbolic Model Checking, Formal Methods in System Design, v.23 n.3, p.303-327, November 2003
Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997
Jia Xu, On Inspection and Verification of Software with Timing Requirements, IEEE Transactions on Software Engineering, v.29 n.8, p.705-720, August 2003
Cormac Flanagan, Automatic software model checking via constraint logic, Science of Computer Programming, v.50 n.1-3, p.253-270, March 2004
Xiushan Feng , Alan J. Hu , Jin Yang, Partitioned model checking from software specifications, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
K. Rustan M. Leino , Todd Millstein , James B. Saxe, Generating error traces from verification-condition counterexamples, Science of Computer Programming, v.55 n.1-3, p.209-226, March 2005
S. Chouali , J. Julliand , P.-A. Masson , F. Bellegarde, PLTL-partitioned model checking for reactive systems under fairness assumptions, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.267-301, May 2005
Paul Caspi , Alain Girault , Daniel Pilaud, Automatic Distribution of Reactive Systems for Asynchronous Networks of Processors, IEEE Transactions on Software Engineering, v.25 n.3, p.416-427, May 1999
Daniel P. Siewiorek , Ram Chillarege , Zbigniew T. Kalbarczyk, Reflections on Industry Trends and Experimental Research in Dependability, IEEE Transactions on Dependable and Secure Computing, v.1 n.2, p.109-127, April 2004
Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Compiling Real-Time Specifications into Extended Automata, IEEE Transactions on Software Engineering, v.18 n.9, p.794-804, September 1992
John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
Samik Basu , C. R. Ramakrishnan, Compositional analysis for verification of parameterized systems, Theoretical Computer Science, v.354 n.2, p.211-229, 28 March 2006
Yonit Kesten , Amir Pnueli , Li-On Raviv , Elad Shahar, Model Checking with Strong Fairness, Formal Methods in System Design, v.28 n.1, p.57-84, January 2006
Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite StateSpaces using QDDs, Formal Methods in System Design, v.14 n.3, p.237-255, May 1999
Jean-François Monin, Proving the Correctness of the Standardized Algorithm for ABR Conformance, Formal Methods in System Design, v.17 n.3, p.221-243, Dec. 2000
Rance Cleaveland , S. Purushothaman Iyer , Murali Narasimha, Probabilistic temporal logics via the modal mu-calculus, Theoretical Computer Science, v.342 n.2-3, p.316-350, 7 September 2005
Sezer Gören , F. Joel Ferguson, Test sequence generation for controller verification and test with high coverage, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.4, p.916-938, October 2006
Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
Hana Chockler , Orna Kupferman , Moshe Y. Vardi, Coverage metrics for temporal logic model checking, Formal Methods in System Design, v.28 n.3, p.189-212, May 2006
R. Janvier , Y. Lakhnech , M. Périn, Certifying cryptographic protocols by abstract model-checking and proof concretization, ACM SIGBED Review, v.3 n.4, p.37-57, October 2006
Hana Chockler , Eitan Farchi , Ziv Glazberg , Benny Godlin , Yarden Nir-Buchbinder , Ishai Rabinovitz, Formal verification of concurrent software: two case studies, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
L. M. Kristensen , K. Schmidt , A. Valmari, Question-guided stubborn set methods for state properties, Formal Methods in System Design, v.29 n.3, p.215-251, November 2006
Fei Xie , Guowu Yang , Xiaoyu Song, Component-based hardware/software co-verification for building trustworthy embedded systems, Journal of Systems and Software, v.80 n.5, p.643-654, May, 2007
Christopher Robinson-Mallett , Robert M. Hierons , Peter Liggesmeyer, Achieving communication coverage in testing, ACM SIGSOFT Software Engineering Notes, v.31 n.6, November 2006
Domagoj Babic , Alan J. Hu, Calysto: scalable and precise extended static checking, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
Flavio M. De Paula , Alan J. Hu, An effective guidance strategy for abstraction-guided simulation, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
Paul Caspi , Norman Scaife , Christos Sofronis , Stavros Tripakis, Semantics-preserving multitask implementation of synchronous programs, ACM Transactions on Embedded Computing Systems (TECS), v.7 n.2, p.1-40, February 2008
Quocnam Tran , Moshe Y. Vardi, Groebner bases computation in Boolean rings for symbolic model checking, Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference: modelling and simulation, p.440-445, May 30-June 01, 2007, Montreal, Canada
Madanlal Musuvathi , Shaz Qadeer, Fair stateless model checking, ACM SIGPLAN Notices, v.43 n.6, June 2008
Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, ACM SIGPLAN Notices, v.42 n.6, June 2007
Moreno Falaschi , Alicia Villanueva, Automatic verification of timed concurrent constraint programs, Theory and Practice of Logic Programming, v.6 n.3, p.265-300, May 2006
Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger, Computing Accumulated Delays in Real-time Systems, Formal Methods in System Design, v.11 n.2, p.137-155, Aug. 1997
Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States
Patrick Cousot , Radhia Cousot, Refining Model Checking by Abstract Interpretation, Automated Software Engineering, v.6 n.1, p.69-95, January 1999
Nikolaj S. Bjørner , Anca Browne , Michael A. Colón , Bernd Finkbeiner , Zohar Manna , Henny B. Sipma , Tomás E. Uribe, Verifying Temporal Properties of Reactive Systems: A STeP Tutorial, Formal Methods in System Design, v.16 n.3, p.227-270, June 2000
Alan J. Hu , Jeremy Casas , Jin Yang, Efficient Generation of Monitor Circuits for GSTE Assertion Graphs, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.154, November 09-13, 2003
Abhik Roychoudhury , I. V. Ramakrishnan, Inductively Verifying Invariant Properties of Parameterized Systems, Automated Software Engineering, v.11 n.2, p.101-139, April 2004
Sonia Flores , Salvador Lucas , Alicia Villanueva, Formal Verification of Websites, Electronic Notes in Theoretical Computer Science (ENTCS), v.200 n.3, p.103-118, May, 2008
Sharon Shoham , Orna Grumberg, A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.1-es, December 2007
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, Formal methods for the analysis and synthesis of nanometer-scale cellular arrays, ACM Journal on Emerging Technologies in Computing Systems (JETC), v.4 n.2, p.1-27, April 2008
Pao-Ann Hsiung , Shang-Wei Lin, Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems, Computer Languages, Systems and Structures, v.34 n.4, p.153-169, December, 2008
Alper Sen , Vijay K. Garg, Formal Verification of Simulation Traces Using Computation Slicing, IEEE Transactions on Computers, v.56 n.4, p.511-527, April 2007
Pao-Ann Hsiung , Yean-Ru Chen , Yen-Hung Lin, Model Checking Safety-Critical Systems Using Safecharts, IEEE Transactions on Computers, v.56 n.5, p.692-705, May 2007
Alastair F. Donaldson , Alice Miller, Automatic Symmetry Detection for Promela, Journal of Automated Reasoning, v.41 n.3-4, p.251-293, November 2008
Hana Chockler , Ofer Strichman, Before and after vacuity, Formal Methods in System Design, v.34 n.1, p.37-58, February 2009
Robert M. Hierons , Kirill Bogdanov , Jonathan P. Bowen , Rance Cleaveland , John Derrick , Jeremy Dick , Marian Gheorghe , Mark Harman , Kalpesh Kapoor , Paul Krause , Gerald Lüttgen , Anthony J. H. Simons , Sergiy Vilkomir , Martin R. Woodward , Hussein Zedan, Using formal specifications to support testing, ACM Computing Surveys (CSUR), v.41 n.2, p.1-76, February 2009
K. L. McMillan, Model checking, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
Hana Chockler , Arie Gurfinkel , Ofer Strichman, Beyond vacuity: towards the strongest passing formula, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
Ariel Cohen , Kedar S. Namjoshi, Local proofs for global safety properties, Formal Methods in System Design, v.34 n.2, p.104-125, April 2009
Parosh Aziz Abdulla , Frédéric Haziza , Mats Kindahl, Model checking race-freeness, ACM SIGARCH Computer Architecture News, v.36 n.5, December 2008
J. Julliand , P. -A. Masson , E. Oudot, Partitioned PLTL model-checking for refined transition systems, Information and Computation, v.207 n.6, p.681-698, June, 2009
Stavros Tripakis, Checking timed Büchi automata emptiness on simulation graphs, ACM Transactions on Computational Logic (TOCL), v.10 n.3, p.1-19, April 2009
Ananda Basu , Matthieu Gallien , Charles Lesire , Thanh-Hung Nguyen , Saddek Bensalem , Félix Ingrand , Joseph Sifakis, Incremental Component-Based Construction and Verification of a Robotic System, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.631-635, June 27, 2008
Orna Grumberg , Shlomi Livne , Shaul Markovitch, Learning to order BDD variables in verification, Journal of Artificial Intelligence Research, v.18 n.1, p.83-116, January 2003
Moshe Y. Vardi, Automated verification: graphs, logic, and automata, Proceedings of the 18th international joint conference on Artificial intelligence, p.1603-1606, August 09-15, 2003, Acapulco, Mexico
Martin Lange, Model Checking for Hybrid Logic, Journal of Logic, Language and Information, v.18 n.4, p.465-491, October 2009
Gordon Fraser , Franz Wotawa , Paul Ammann, Issues in using model checkers for test case generation, Journal of Systems and Software, v.82 n.9, p.1403-1418, September, 2009
Edmund M. Clarke , E. Allen Emerson , Joseph Sifakis, Model checking: algorithmic verification and debugging, Communications of the ACM, v.52 n.11, November 2009
Ranjit Jhala , Rupak Majumdar, Software model checking, ACM Computing Surveys (CSUR), v.41 n.4, p.1-54, October 2009
Collaborative Colleagues:
Jean-Pierre Queille: colleagues
Joseph Sifakis: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player