Registro:

Referencias:

• Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D., (2004) Evaluating the "small Scope Hypothesis", , http://mulsaw.lcs.mit.edu/papers/SSH.ps, Unpublished. (Last accessed 11/2012)
• Arkoudas, K., (2001) Type-ω DPLs, , MIT AI Memo 2001-27. Massachusetts Institute of Technology, Cambridge, MA
• Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M., Integrating model checking and theorem proving for relational reasoning (2004) Proceedings of the 7th Conference on Relational Methods in Computer Science (RelMiCS) - 2nd International Workshop on Applications of Kleene Algebra, 3051, pp. 204-213. , http://dx.doi.org/10.1007/978-3-540-24771-5_3, R. Berghammer and B. Möller, Eds., Lecture Notes in Computer Science, Springer-Verlag
• Beckert, B., Hähnle, R., Schmitt, P.H., (2007) Verification of Object-Oriented Software: The KeY Approach, , http://dx.doi.org/10.1007/978-3-540-69061-0, Springer-Verlag
• Bertot, Y., Castéran, P., (2004) Interactive Theorem Proving and Program Development - coq'Art: The Calculus of Inductive Constructions, , http://dx.doi.org/10.1007/978-3-662-07964-5, EATCS Texts in Theoretical Computer Science
• Blanchette, J., Nipkow, T., Nitpick: A counterexample generator for higher-order logic based on a relational model finder (2010) Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010), 6172, pp. 131-146. , http://dx.doi.org/10.1007/978-3-642-14052-5_11, Lecture Notes in Computer Science, Springer
• Edmund, M., Orna Grumberg, C., Peled, D.A., (1999) Model Checking, , MIT Press
• De Moura, L., Bjorner, N., Z3: An efficient SMT solver (2008) Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 4963, pp. 337-340. , http://dx.doi.org/10.1007/978-3-540-78800-3_24, Lecture Notes in Computer Science, Springer, Berlin
• Aboubakr, A., Ghazi, E., Taghdiri, M., Relational reasoning via SMT solving (2011) Proceedings of the International Symposium on Formal Methods (FM), 6664, pp. 133-148. , http://dx.doi.org/10.1007/978-3-642-21437-0_12, Lecture Notes in Computer Science, Springer, Berlin
• Frias, M.F., Fork Algebras in algebra, Logic and Computer science (2002) Advances in Logic, 2. , http://dx.doi.org/10.1142/4899, World Scientific Publishing Co
• Frias, M.F., Haeberer, A.M., Veloso, P.A.S., A finite axiomatization for fork algebras (1997) Logic J. IGPL, 5 (3), pp. 311-319. , http://dx.doi.org/10.1093/jigpal/5.3.1
• Frias, M.F., Lopez Pombo, C.G., Aguirre, N.M., An equational calculus for Alloy (2004) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3308, pp. 162-175
• Frias, M.F., Lopez Pombo, C.G., Moscato, M.M., Alloy Analyzer+PVS in the analysis and verification of Alloy specifications (2007) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), LNCS 4424, pp. 587-601. , Tools and Algorithms for the Construction and Analysis of Systems - 13th International Conference, TACAS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007
• Gentzen, G., Untersuchungen über das logische Schließen (1935) Mathematische Zeitschrift, 39, pp. 176-210. , 405-431
• Szabo, M.E., (1969) The Collected Papers of Gerhard Gentzen, 55, pp. 68-131. , http://dx.doi.org/10.1016/S0049-237X(08)70822-X, Studies in Logic and the Foundations of Mathematics. Elsevier
• Michael, J., Gordon, C., Mechanizing programming logics in higher order logic (1989) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387-439. , http://dx.doi.org/10.1007/978-1-4612-3658-0_10, Graham Birtwistle and P. A. Subrahmanyam (Eds.), Springer, New York, NY
• Holzmann, G.J., (2003) The SPIN Model Checker: Primer and Reference Manual, , (1st. ed.). Addison-Wesley Professional
• Jackson, D., Shlyakhter, I., Sridharan, M., A micromodularity mechanism (2001) Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 62-73
• Jackson, D., (2012) Software Abstractions: Logic, Language, and Analysis, , http://dx.doi.org/10.1007/s10270-012-0259-7, (Revised version). The MIT Press
• Kaufmann, T., McConnell, C., Vazquez, I., Antoniotti, M., Campbell, R., Amoroso, P., (2000) ILISP User Manual, , http://library.isr.ist.utl.pt/docs/ilisp/ilisp_toc.html, (Last accessed 11/2012)
• Maddux, R.D., Pair-dense relation algebras (1991) Trans. AMS, 328 (1), pp. 83-131. , http://dx.doi.org/10.2307/2001878
• Moscato, M.M., López Pombo, C.G., Frias, M.F., Dynamite 2.0: New features based on UnSAT-Core extraction to improve verification of software requirements (2010) Proceedings of the International Conference on Theoretical Aspects of Computing (ICTAC 2010), 6255, pp. 275-289. , http://dx.doi.org/10.1007/978-3-642-14808-8_19, Lecture Notes in Computer Science, Springer-Verlag, Berlin
• Nipkow, T., Wenzel, M., Paulson, L.C., (2002) Isabelle/HOL - A Proof Assistant for Higher-Order Logic, 2283. , http://dx.doi.org/10.1007/3-540-45949-9, Lecture Notes in Computer Science, Springer-Verlag, Berlin
• Owre, S., A brief overview of the PVS user interface (2008) Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP'08)
• Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J., (2001) PVS Prover Guide, , Version 2.4. Computer Science Laboratory, SRI International, Menlo Park, CA
• Owre, S., Rushby, J.M., Shankar, N., PVS: A prototype verification system (1992) Proceedings of the 11th International Conference on Automated Deduction, 607, pp. 748-752. , http://dx.doi.org/10.1007/3-540-55602-8_217, Lecture Notes in Artificial Intelligence, Springer
• Ramananandro, T., Mondex, an electronic purse: Specification and refinement checks with the Alloy model-finding method (2008) Formal Aspects of Comput., 20 (1), pp. 21-39. , http://dx.doi.org/10.1007/s00165-007-0058-z
• Torlak, E., Chang, F., Jackson, D., Finding minimal unsatisfiable cores of declarative specifications (2008) Proceedings of the 15th International Symposium on Formal Methods, 5014, pp. 326-341. , http://dx.doi.org/10.1007/978-3-540-68237-0_23, Lecture Notes in Computer Science, Springer, Berlin
• Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M., A proof assistant for alloy specifications (2012) Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 7214, pp. 422-436. , http://dx.doi.org/10.1007/978-3-642-28756-5_29, Lecture Notes in Computer Science, Springer, Berlin
• Zave, P., Compositional binding in network domains (2006) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), LNCS 4085, pp. 332-347. , FM 2006: Formal Methods - 14th International Symposium on Formal Methods, Proceedings

Citas:

---------- APA ----------

---------- CHICAGO ----------

---------- MLA ----------

---------- VANCOUVER ----------