This work is done in the context of ESPRIT Basic Research Action 7166, CONCUR2. Also the work has been supported in part by the Danish Natural Science Research Council through the DART project.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H.R. Andersen. Model checking and boolean graphs. Lecture Notes In Computer Science, Springer Verlag, 1992. In Proceedings of CAAP'92.
M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20, 1983.
T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14, 1987.
J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.
Meyer Bloom, Istrail. bisimulation can't be traced. Proceedings of Principles of Programming Languages, 1988.
G. Boudol. Calcul de processus et verification. Technical Report 424, INRIA, 1985.
R. Cleaveland. Tableau-based model checkin in the prepositional mu-calculus. Acta Informatica, 1990.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. University of Edinburgh, Scotland, 1988.
R. Cleaveland and B. Steffen. Computing behavioural relations, logically. Lecture Notes In Computer Science, Springer Verlag, 510, 1991.
R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for ethe alternation-free modal mu-calculus. Lecture Notes In Computer Science, Springer Verlag, 1991. To appear in Proceedings of Third Workshop on Computer Aided Verification.
E.M.Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS, 8(2), 1986.
E.A. Emerson and C.L Lei. Efficient model checking in fragments of the prepositional mu-calculus. Proceedings of Logic in Computer Science, 1986.
J.C. Fernandez and L. Mounier. A tool set for deciding beharioural equivalence. Lecture Notes In Computer Science, Springer Verlag, 527, 1991.
P. Godefroid and P. Wolper. A partial approach to model-checking. In Proceedings of Logic in Computer Science, 1991.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Lecture Notes In Computer Science, Springer Verlag, 1991. To appear in Proceedings of Third workshop on Computer Aided Verification.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
H. Hültel and C. Stirling. Actions speak louder than words: proving bisimilarity for context-free processes. Proceedings of Logic in Computer Science, 1991.
K.G. Larsen J.C. Godskesen and M. Zeeberg. Tav — tools for automatic verification — users manual. Technical Report R 89-19, Department of Mathematics and Computer Science, Aalborg University, 1989. Presented at workshop on Automatic Methods for Finite State Systems, Grenoble, France, Juni 1989.
D. Kozen. Results on the prepositional mu-calculus. Lecture Notes In Computer Science, Springer Verlag, 140, 1982. in Proc. of International Colloquium on Algorithms, Languages and Programming 1982.
K.G. Larsen. A context dependent bisimulation between processes. Theoretical Computer Science, 49, 1987.
K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72, 1990.
V. Lecompte, E. Madelaine, and D. Vergamini. Auto: A verfication system for parallel and communicating processes. INRIA, Sophia-Antipolis, 1988.
K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1), 1991.
Kim G. Larsen and Bent Thomsen. A modal process logic. In Proceeding on Logic in Computer Science, 1988.
K.G. Larsen and L. Xinxin. Equation solving using modal transition systems. In Proceedings on Logic in Computer Science, 1990.
R. Milner. Calculus of Communicating Systems, volume 92 of Lecture Notes In Computer Science, Springer Verlag. Springer Verlag, 1980.
R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
D. Park. Concurrency and automata on infinite sequences. Lecture Notes In Computer Science, Springer Verlag, 104, 1981. Proceedings of 5th GI Conference.
J. Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68, 1989.
G. Plotkin. A structural approach to operational semantics. FN 19, OAIMI, Aarhus University, Denmark, 1981.
A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. Lecture Notes In Computer Science, Springer Verlag, 194, 1985. Proceedings of 12th International Colloquium on Automata, Languages and Programming.
P.C.Kanellakis and S.A.Smolka. Ces expressions, finite state processes, and three problems of equivalence. Information and Control, 86, 1990.
Paige and Tarjan. Three partition refinement algorithms. SIAM Journal of Computing, 16(6), 1987.
J.L. Rixchier, C. Rodriguez, J. Sifakis, and J. Voiron. Xesar: a tool for protocol validation. users' guide. Technical report, LGI-IMAG, 1987.
M.W. Shields. A note on the simple interface equation. Technical report, University of Kent at Canterbury.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Lecture Notes In Computer Science, Springer Verlag, 352, 1989. In Proc. of Tapsoft'89.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.
G. Winskel. Model checking the modal nu-calculus. Lecture Notes In Computer Science, Springer Verlag, 372, 1989. In Proceedings of International Colloquium on Algorithms, Languages and Programming 19'89.
Liu Xinxin. Specification and Decomposition in Concurrency. PhD thesis, Aalborg University, 1992. R 92-2005.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsen, K.G. (1993). Efficient local correctness checking. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_4
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive