Journal of Automated Reasoning

, Volume 51, Issue 3, pp 241–280 | Cite as

Specification and Verification of Concurrent Programs Through Refinements

  • Sandip Ray
  • Rob Sumners


We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.


Abstraction Fairness Reactive systems Theorem proving Trace containment 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comp. Sci. 82(2), 253–284 (1991)MathSciNetCrossRefMATHGoogle Scholar
  2. 2.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  3. 3.
    Arora, N.S., Blumofe, R.D., Plaxton, C.G.: Thread scheduling in multiprogramming multiprocessors. Theory Comput. Syst. 34, 115–144 (2001)MathSciNetMATHGoogle Scholar
  4. 4.
    Attie, P.: Liveness-preserving simulation relations. In: Welch, J. (ed.) Proceedings of 18th ACM Symposium on Principles of Distributed Computing (PODC 1999), pp. 63–72. ACM Press, New York (1999)CrossRefGoogle Scholar
  5. 5.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop on Model Checking of Software. LNCS, vol. 2057, pp. 103–122. Springer, New York (2001)Google Scholar
  6. 6.
    Blumofe, R.D., Leiserson, C.E.: Scheduling multithreaded computations by work stealing. J. ACM 46(5), 720–748 (1999)MathSciNetCrossRefMATHGoogle Scholar
  7. 7.
    Blumofe, R.D., Plaxton, C.G., Ray, S.: Verification of a concurrent deque implementation. Technical report TR-99-11, Department of Computer Sciences, The University of Texas at Austin (1999)Google Scholar
  8. 8.
    Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)MATHGoogle Scholar
  9. 9.
    Boyer, R.S., Goldshlag, D., Kaufmann, M., Moore, J.S.: Functional instantiation in first order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7–26. Academic, New York (1991)CrossRefGoogle Scholar
  10. 10.
    Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A.L., Somenzi, F., Aziz, A., Cheng, S., Edwards, S.A., Khatri, S.P., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T. (eds.) Proceedings of the 8th International Conference on Computer-Aided Verification (CAV 1996). LNCS, vol. 1102, pp. 428–432. Springer, New York (1996)CrossRefGoogle Scholar
  11. 11.
    Brock, B., Hunt, W.A., Jr.: Formally specifying and mechanically verifying programs for the motorola complex arithmetic processor DSP. In: Proceedings of the 1997 International Conference on Computer Design: VLSI in Computers & Processors (ICCD 1997), pp. 31–36, Austin, TX (1997). IEEE Computer Society Press, Los AlamitosGoogle Scholar
  12. 12.
    Bronevetsky, G., Marques, D., Pingali, K., Szwed, P., Schulz, M.: Application-level checkpointing for shared memory programs. In: Mukherjee, S., McKinley, K. (eds.) Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2004), pp. 235–247. ACM Press, New York (2004)Google Scholar
  13. 13.
    Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover, New York (1952, Translated by P.E.B. Jourdain)Google Scholar
  14. 14.
    Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Trans Comput Syst 3(1), 63–75 (1985)CrossRefGoogle Scholar
  15. 15.
    Chandy, K.M., Misra, J.: The drinking philosopher’s problem. ACM Trans. Program. Lang. Syst. (ACM TOPLAS) 6(4), 632–646 (1984)CrossRefGoogle Scholar
  16. 16.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Cambridge (1990)Google Scholar
  17. 17.
    Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA+ proof system. In: Giesl, J., Hähnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010). LNCS, no. 6173, pp. 142–148. Springer, New York (2010)CrossRefGoogle Scholar
  18. 18.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model-Checking. MIT Press, Cambridge (2000)Google Scholar
  19. 19.
    Davis, J.: Finite set theory based on fully ordered lists. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004) (2004)Google Scholar
  20. 20.
    Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Inform. 1(2), 115–138 (1971)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994), pp. 70–83. ACM Press, New York (1994)CrossRefGoogle Scholar
  22. 22.
    Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D. (ed.) Proceedings of the 12th International Conference on Correct Hardware Design and Verification Methods (CHARME 2003). LNCS, vol. 2860, pp. 247–262. Springer, New York (2003)CrossRefGoogle Scholar
  23. 23.
    Emerson, E.A., Namjoshi, K.: Reasoning about rings. In: Ernst, M. (ed.) Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995), pp. 84–95. ACM Press, New York (1995)Google Scholar
  24. 24.
    Engelhardt, K., de Roever, W.P.: Generalizing Abadi & Lamport’s method to solve a problem posed by Pnueli. In: Woodcock, J., Larsen, P.G. (eds.) Industrial-Strength Formal Methods, 1st International Symposium of Formal Methods Europe. LNCS, vol. 670, pp. 294–313, Odense, Denmark. Springer, New York (1993)CrossRefGoogle Scholar
  25. 25.
    Goldshlag, D.M.: Mechanically verifying concurrent programs with the Boyer–Moore prover. IEEE Trans. Softw. Eng. 16(9), 1005–1023 (1990)CrossRefGoogle Scholar
  26. 26.
    Gordon, M.J.C., Hunt, W.A., Jr., Kaufmann, M., Reynolds, J.: An integration of HOL and ACL2. In: Gupta, A., Manolios, P. (eds.) Proceedings on the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2006), pp. 153–160. IEEE Computer Society Press, Los Alamitos (2006)CrossRefGoogle Scholar
  27. 27.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997), LNCS, vol. 1254, pp. 72–83. Springer, New York (1997)CrossRefGoogle Scholar
  28. 28.
    Gupta, A.: Formal hardware verification methods: a survey. Form. Method Syst. Des. 2(3), 151–238 (1992)CrossRefGoogle Scholar
  29. 29.
    Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M., Woodcock, J. (eds.) Proceedings of the 3rd Intermational Symposium of Formal Methods Europe (FME 1996), LNCS, vol. 1051, pp. 662–681. Springer, New York (1996)Google Scholar
  30. 30.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM-SIGPLAN Conference on Principles of Programming Languages (POPL 2002), pp. 58–70. ACM Press, New York (2002)Google Scholar
  31. 31.
    Hesselink, W.: Eternity variables to simulate specification. In: Proceedings of Mathematics of Program Construction. LNCS, vol. 2386, pp. 117–130, Dagstuhl, Germany. Springer, New York (2002)CrossRefGoogle Scholar
  32. 32.
    Hooman, J.: Compositional verification of timed components using PVS. In: Biel, B., Gruhn, V. (eds.) Software Engineering 2006, Fachtagung des GI-Fachbereichs Softwaretechnik. LNI, vol. 79, pp. 143–154 (2006)Google Scholar
  33. 33.
    Jackson, P.B.: Verifying a garbage collector algorithm. In: Grundy, J., Newer, M. (eds.) Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 1998). LNCS, vol. 1479, pp.225–244. Springer, New York (1998)CrossRefGoogle Scholar
  34. 34.
    Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distrib. Comput. 12(2–3), 129–149 (1999)Google Scholar
  35. 35.
    Kaufmann, M., Moore, J.S.: ACL2 home page. See URL (1997)
  36. 36.
    Kaufmann, M., Moore, J.S.: A precise description of the ACL2 logic. See URL (1997)
  37. 37.
    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Boston (2000)Google Scholar
  38. 38.
    Kaufmann, M., Sumners, R.: Efficient rewriting of data structures in ACL2. In: Borrione, D., Kaufmann, M., Moore, J.S. (eds.) Proceedings of 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), pp. 141–150. Grenoble, France (2002)Google Scholar
  39. 39.
    Kern, C., Greenstreet, M.: Formal verification in hardware design: a survey. ACM Transact. Des. Automat. Electron. Syst. 4(2), 123–193 (1999)CrossRefGoogle Scholar
  40. 40.
    Kyas, M., Hooman, J.: A semantics of communicating reactive objects with timing. Softw. Tools Technol. Transf. (STTT) 8(4), 97–112 (2006)Google Scholar
  41. 41.
    Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer-Aided Verification (CAV 2004). LNCS, vol. 3117, pp. 135–147. Springer, New York (2004)CrossRefGoogle Scholar
  42. 42.
    Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Proceedings of the 15th International Conference on Computer-Aided Verification. LNCS, vol. 2275, pp. 141–153. Springer, New York (2003)CrossRefGoogle Scholar
  43. 43.
    Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974)MathSciNetCrossRefMATHGoogle Scholar
  44. 44.
    Lamport, L.: What good is temporal logic? Inf. Process. 83, 657–688 (1983)Google Scholar
  45. 45.
    Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. (ACM TOPLAS) 16(3), 827–923 (1994)Google Scholar
  46. 46.
    Lamport, L., Matthews, J., Tuttle, M., Yu, Y.: Specifying and verifying systems with TLA+. In: Jul, E. (ed.) Proceedings of the 10th ACM SIGOPS European Workshop, pp. 45–48. Copenhagen, Denmark (2002)CrossRefGoogle Scholar
  47. 47.
    Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1996)MATHGoogle Scholar
  48. 48.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)CrossRefGoogle Scholar
  49. 49.
    Manolios, P.: Mechanical verification of reactive systems. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (2001)Google Scholar
  50. 50.
    Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D. (ed.) Proceedings of the 12th Working Conference on Correct Hardware Design and Verification Methods. LNCS, vol. 2860, pp. 304–218. Springer, New York (2003)Google Scholar
  51. 51.
    Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) Proceedings of the 19th International Conference on Automated Deduction (CADE 2003). LNAI, vol. 2741, pp. 243–257, Miami, FL. Springer, New York (2003)Google Scholar
  52. 52.
    Manolios, P., Namjoshi, K., Sumners, R.: Linking model-checking and theorem-proving with well-founded bisimulations. In: Halbwacha, N., Peled, D. (eds.) Proceedings of the 11th International Conference on Computer-Aided Verification (CAV 1999). LNCS, vol. 1633, pp. 369–379. Springer, New York (1999)CrossRefGoogle Scholar
  53. 53.
    McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)CrossRefMATHGoogle Scholar
  54. 54.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)Google Scholar
  55. 55.
    Misra, J.: A logic of concurrent programing: progress. J. Comput. Softw. Engin. 3(2), 273–300 (1995)Google Scholar
  56. 56.
    Misra, J.: A logic of concurrent programing: safety. J. Comput. Softw. Engin. 3(2), 239–372 (1995)Google Scholar
  57. 57.
    Misra, J.: A discipline of multiprogramming: programming theory for distributed applications. In: Monographs in Computer Science. Springer, New York (2001)Google Scholar
  58. 58.
    Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, pp. 227–290. IOS Press, Amsterdam (2003)Google Scholar
  59. 59.
    Moore, J.S., Porter, G.: The apprentice challenge. ACM Transac. Program. Lang. Syst. (ACM TOPLAS) 24(3), 1–24 (2002)Google Scholar
  60. 60.
    Namjoshi, K.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) Proceedings of the 17th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1997). LNCS, vol. 1346, pp. 284–296. Springer, New York (1997)CrossRefGoogle Scholar
  61. 61.
    Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV 2000). LNCS, vol. 1855, pp. 435–449. Springer, New York (2000)CrossRefGoogle Scholar
  62. 62.
    Park, D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, New York (1981)CrossRefGoogle Scholar
  63. 63.
    Paulson, L.: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1), 3–32 (2000)MathSciNetCrossRefGoogle Scholar
  64. 64.
    Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Proceedings of the 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001). LNCS, vol. 2031, pp. 82–97. Springer, New York (2001)CrossRefGoogle Scholar
  65. 65.
    Ray, S., Sumners, R.: Combining theorem proving with model checking through predicate abstraction. IEEE Des. Test Comput. 24(2), 132–139 (2007)CrossRefGoogle Scholar
  66. 66.
    Ray, S., Sumners, R.: A theorem proving approach for verification of reactive concurrent programs. In: Burckhardt, S., Chaudhury, S., Farzan, A., Gopalakrishnen, G., Seigel, S. (eds.) 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 2011) (2011)Google Scholar
  67. 67.
    Russinoff, D.: A mechanically verified incremental garbage collector. Form. Asp. Comput. 6, 359–390 (1994)CrossRefMATHGoogle Scholar
  68. 68.
    Sawada, J., Hunt, W.A., Jr.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997). LNCS, vol. 1254, pp. 364–375. Springer, New York (1997)CrossRefGoogle Scholar
  69. 69.
    Shankar, N.: Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 571, pp. 217–236. Springer, New York (1992)CrossRefGoogle Scholar
  70. 70.
    Sumners, R.: An incremental stuttering refinement proof of a concurrent program in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) 2nd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2000). Austin, TX (2000)Google Scholar
  71. 71.
    Sumners, R.: Fair environment assumptions in ACL2. In: Hunt, W.A., Jr., Kaufmann, M., Moore, J.S. (eds.) 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003). Boulder, CO (2003)Google Scholar
  72. 72.
    Sumners, R., Ray, S.: Reducing invariant proofs to finite search via rewriting. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004). Austin, TX (2004)Google Scholar
  73. 73.
    Sumners, R., Ray, S.: Proving invariants via rewriting and abstraction. Technical report TR-05-35, Department of Computer Sciences, University of Texas at Austin (2005)Google Scholar
  74. 74.
    Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. J. 10(2), 203–232 (2003)CrossRefGoogle Scholar
  75. 75.
    Wansbrough, K., Norrish, M., Sewell, P., Serjantov, A.: Timing UDP: mechanized semantics of sockets, threads and failures. In: Le Métayer, D. (ed.) Proceedings of the 11th European Symposium on Programming (ESOP 2002). LNCS, vol. 2305, pp. 178–294. Springer, New York (2002)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2012

Authors and Affiliations

  1. 1.Strategic CAD LabsIntel CorporationHillsboroUSA
  2. 2.Advanced Micro Devices, Inc.AustinUSA

Personalised recommendations