Deductive verification of alternating systems

Alur R, Henzinger TA, Kupferman O (1999) Alternating-time temporal logic. In: FOCS, pp 100–109, 1997. An extended version appeared in compositionality—the significant difference, vol 1536. LNCS. Springer, Heidelberg, pp 23–60 Alur R, Henzinger TA, Kupferman O(2002) Alternating-time temporal logic. J ACM 49(5):672–713 Alur R, Henzinger TA, Kupferman O, Vardi MY (1998) Alternating refinement relations. In: Sangiorgi D, de Simone R (eds) CONCUR, vol 1466, LNCS. Springer, Heidelberg, pp 163–178 Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S (1998) Mocha: modularity in model checking. In: Proceedings of 10th international conference on computer aided verification, vol 1427, LNCS. Springer, Heidelberg, pp 516–520 Asokan N, Shoup V, Waidner M (1998) Asynchronous protocols for optimistic fair exchange. In: Proceedings of the IEEE symposium on security and privacy Bjørner NS, Browne A, Manna Z (1997) Automatic generation of invariants and intermediate assertions. Theor Comput Sci 173(1):49–87, February 1997. Preliminary version appeared in 1st International Conference on Principles and Practice of Constraint Programming, vol. 976, LNCS (1995). Springer, Heidelberg, pp 589–623 Backes M, Datta A, Derek A, Mitchell JC, Turuani M (2004) Compositional analysis of contract signing protocols. In: Proceedings of the 18th IEEE computer security foundation workshop, pp 30–45 Ben-Ari M, Manna Z, Pnueli A (1981) The temporal logic of branching time. In: PoPL. ACM Press, pp 164–176 Browne A, Manna Z, Sipma HB (1995) Generalized temporal verification diagrams. In: 15th conference on the foundations of software technology and theoretical computer science, vol 1026, LNCS. Springer, Heidelberg, pp 484–498 Baum-Waidner B, Waidner M (2000) Round-optimal and abuse-free optimistic multi-party contract signing. In: Ugo Montanari, José D.P. Rolim, Emo Welzl (eds) 27th International Colloquium on Automata, Languages and Programming (ICALP2000), vol 1853, LNCS. Springer, Heidelberg, pp 524–535 Clarke EM Jr, Grumberg O, Peled DA (1999) Model Checking. MIT Press, Cambridge Chandra AK, Kozen DC, Stockmeyer LJ (1981) Alternation. J ACM 28:114–133 Chadha R, Kremer S, Scedrov A (2006) Formal analysis of multi-party contract signing. J Autom Reason 36(1–2):39–83 Cook SA (1978) Soundness and completeness of an axiom system for program verification. SIAM J Comput 7(1):70–90 Chandra AK, Stockmeyer LJ (1976) Alternation. In: FOCS. IEEE computer society, pp 98–108 Davis M (1964) Infinite games of perfect information. In: Dresher M, Shapley LS, Tucker AW (eds) Advances in Game Theory, number 52, Annal of Mathematics Studies. Princeton University Press, New Jersey, pp 85–101 Datta A, Derek A, Mitchell JC, Pavlović D (2004) Secure protocol composition. In: Proceedings of the 19th annual conference on mathematical foundatinons of programming semantics, number 83, Electronic Notes in Theoretical Computer Science Emerson EA, Clarke EM, Jr (1980) Characterizing correctness properties of parallel programs using fixpoints. In: ICALP, vol 85, LNCS. Springer, Heidelberg, pp 169–181 Emerson EA, Clarke EM, Jr (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comp. Prog. 2(3):241–266 Emerson EA, Halpern JY (1986) ‘Sometimes’ and ‘not never’ revisited: on branching time versus linear time. J ACM 33: 151–178 Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of Theoretical Computer Science, vol B. Elsevier, Amsterdam, pp 995–1072 Fix L, Grumberg O (1996) Verification of temporal properties. J Logic Comput 6(3):343–361 Finkbeiner BE (2002) Verification algorithms based on alternating automata. PhD thesis, Stanford University Floyd RW (1967) Assigning meanings to programs. In: Mathematical aspects of computer science, vol 19, Proceedings of symposia in applied mathematics. American Mathematical Society, pp 19–32 Finkbeiner BE, Schewe S (2005) Uniform distributed synthesis. In: LICS, pp 321–330 Gurevich Y, Harrington L (1982) Trees, automata, and games. In: STOC, pp 60–65 Gabbay DM, Pnueli A, Shelah S, Stavi J (1980) On the temporal analysis of fairness. In: POPL. ACM Press, pp 163–173 Gale D, Stewart FM (1953) Infinite games with perfect information. Ann Math Stud 28:245–266 Goranko V, van Drimmelen G (2006) Complete axiomatization and decidability of alternating-time temporal logic. Theor Comput Sci 353(1–3):93–117 Henzinger TA, Majumdar R, Mang FYC, Raskin J-F (2000) Abstract interpretation of game properties. In: Proceedings of 7th international static analysis symposium (SAS), vol 1824, LNCS. Springer, Heidelberg, pp 220–239 Harel D, Meyer AR, Pratt VR (1977) Computability and completeness in logics of programs. In: STOC, pp 261–268 Richard Hoare CA (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–583 Harel D, Pnueli A, Stavi J (1977) A complete axiomatic system for proving deductions about recursive programs. In: STOC, pp 249–260 Kozen D (1976) On parallelism in turing machines. In: FOCS. IEEE Computer Society, pp 89–97 Kozen DC (1983) Results on the propositional μ-calculus. Theor Comput Sci 27(3):333–354 Kesten Y, Pnueli A (2005) A compositional approach to CTL* verification. Theor Comput Sci 331:397–428 Kremer S, Raskin J-F (2002) Game analysis of abuse-free contract signing. In: Computer security foundations workshop (CSFW). IEEE Computer Society Kremer S, Raskin J-F (2003) A game-based verification of non-repudiation and fair exchange protocols. J Comput Security 11(3):399–429 Kuratowski C (1958) Topologie, vol I. Państwowe Wydawnictwo Naukowe, 4th edn Kuratowski C (1961) Topologie, vol I. Państwowe Wydawnictwo Naukowe, 3rd edn Lamport L (2002) Specifying systems. Addison-Wesley, Reading Lehmann D, Pnueli A, Stavi J (1981) Impartiality, justice and fairness: The ethics of concurrent termination. In: Shimon Even and Oded Kariv, editors, Automata, Languages and Programming—8th International colloquium, ICALP, vol 115, LNCS. Springer, Heidelberg, pp 264–277 Martin DA (1975) Borel determinacy. Ann Math 102:363–371 Martin DA (1985) A purely inductive proof of borel determinacy. In: Proceedings of symposia in pure mathematics, vol 42. American Mathematical Society, pp 303–308 Manna Z, Browne A, Sipma HB, Uribe TE (1998) Visual abstractions for temporal verification. In: Haeberer A (ed) AMAST, vol 1548, LNCS. Springer, Heidelberg, pp 28–41 McNaughton R (1993) Infinite games played on finite graphs. Ann Pure Appl Logic 65:149–184 Mitchell JC (1996) Foundations of programming languages. Foundations of computing. MIT Press, Cambridge Manna Z, Pnueli A (1983) Verification of concurrent programs: a temporal proof system. In: Jaco W, de Bakker and Van Leeuwen J (eds) Foundations of computer science IV, distributed systems: Part 2. Mathematical Centre Tracts 159. Center for Mathematics and Computer Science (CWI), Amsterdam, pp 163–255 Manna Z, Pnueli A (1989) Completing the temporal picture. In: Ausiello G, Dezani-Ciancaglini M, Della Rocca SR (eds) 16th International colloquium on automata, languages, and programming, vol 372, LNCS. Springer, Heidelberg, pp 534–558 Manna Z, Pnueli A (1991) The temporal logic of reactive and concurrent systems: specification. Springer, Heidelberg Manna Z, Pnueli A (1994) Temporal verification diagrams. In: Proceedings of international symposium on theoretical aspects of computer software, vol 789, LNCS. Springer, Heidelberg, pp 726–765 Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Heidelberg Manna Z, Pnueli A (1996) Temporal verification of reactive systems: progress. Draft. Available on line at http://theory.stanford.edu/~zm/tvors3.html Mahimkar A, Shmatikov V (2005) Game-based analysis of denial-of-service prevention protocols. In: Computer Security Foundations Workshop (CSFW). IEEE Computer Society Osborne MJ, Rubinstein A (1994) A course in game theory. MIT Press, Cambridge Parikh R (1985) The logic of games and its applications. Ann Discrete Math 24:111–140 Pnueli A, Kesten Y(2002) A deductive proof system for CTL*. In: Brim L, Jančar P, Křetínský M, Kučera A (eds) CONCUR 2002—concurrency theory: 13th international conference, vol 2421, LNCS. Springer, Heidelberg, pp 24–40 Pnueli A (1977) The temporal logic of programs. In: FOCS. IEEE Computer Society, pp 46–57 Rabin MO (1969) Decidability of second order theories and automata on infinite trees. Trans AMS 141:1–35 Reynolds M (2000) An axiomatization of full computation tree logic. J Symbol Logic 66(3):1011–1057 Sankaranarayanan S (2005) Mathematical analysis of programs. PhD thesis, Stanford University Stomp FA, de Roever W-P, Gerth RT (1989) The μ-calculus as an assertion language for fairness arguments. Inf Comput 82(3):278–322 Sipma HB (1999) Diagram-based verification of discrete, real-time and hybrid systems. PhD thesis, Computer Science Department, Stanford University Slanina M (2002) Control rules for reactive system games. In: Fischer B, Smith DR (eds) Logic-based program synthesis: state of the art and future trends, AAAI spring symposium. The American Association for Artificial Intelligence, AAAI Press, March 2002. Available from AAAI as Technical Report SS-02-05, pp 95–104 Slanina M (2007) Deductive verification of alternating systems. PhD thesis, Stanford University Slanina M, Sipma HB, Manna Z (2006) Game-theoretic deductive verification of a contract-signing protocol. Technical Report REACT-TR-2006-03, Stanford University, Computer Science Department, REACT Group, August 2006. Available at http://react.stanford.edu/TR/. Slanina M, Sipma HB, Manna Z (2006) Game-theoretic deductive verification of a contract-signing protocol II. Technical Report REACT-TR-2006-04, Stanford University, Computer Science Department, REACT Group, August 2006. Available at http://react.stanford.edu/TR/ Slanina M, Sipma HB, Manna Z (2006) Proving ATL* properties of infinite-state systems. In: Barkaui K, Cavalcanti A, Cerone A (eds) 3rd International colloquium on theoretical aspects of computing (ICTAC2006), vol 4281, LNCS. Springer, Heidelberg, pp 242–256 Thomas W (1995) On the synthesis of strategies in infinite games. In: Mayr EW, Puech C (eds) Proceedings of the 12th annual symposium on theoretical aspects of computer science, STACS ’95, vol 900, LNCS. Springer, Heidelberg, pp 1–13 Thomas W (1997) Languages, automata, and logic. In: Rozenberg G, Salomaa A (eds) Handbook of formal languages, vol 3, Chap 7. Springer, Heidelberg, pp 389–455 Troelstra AS, Schwichtenberg H (2000) Basic proof theory. Cambridge University Press, 2nd edn Vardi MY (1991) Verification of concurrent programs: the automata-theoretic framework. J Pure Appl Logic 51(1–2):79–98 Vardi MY (1995) Alternating automata and program verification. In: van Leeuwen J (ed) Computer science today: recent trends and developments, vol 1000, LNCS. Springer, Heidelberg, pp 471–485 Wikipedia. Gomoku. http://en.wikipedia.org/wiki/Gomoku. Retrieved on February 17, 2007 Wolfe P (1955) The strict determinateness of certain infinite games. Pacific J Math, 5(Supplement I), Zielonka W (1998) Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor Comput Sci 200:135–183