Alex David Groce's Publications

Journal Papers

  1. Exploiting Traces in Static Program Analysis: Better Model Checking through printfs

    Alex Groce and Rajeev Joshi. "Exploiting Traces in Static Program Analysis: Better Model Checking through printfs." International Journal on Software Tools for Technology Transfer, online first, January 2008.

  2. Adaptive Model Checking

    Alex Groce, Doron Peled, and Mihalis Yannakakis. "Adaptive Model Checking." Logic Journal of the IGPL, Volume 14, Number 5, pages 729-744, October 2006.

  3. Error Explanation with Distance Metrics

    Alex Groce, Sagar Chaki, Daniel Kroening, and Ofer Strichman. "Error Explanation with Distance Metrics." International Journal on Software Tools for Technology Transfer, Volume 8, Number 3, pages 229--247, June 2006.

  4. Heuristics for Model Checking Java Programs

    Alex Groce and Willem Visser. "Heuristics for Model Checking Java Programs." International Journal on Software Tools for Technology Transfer, Volume 6, Number 4, pages 260--276, August 2004.

  5. Efficient Verification of Sequential and Concurrent C Programs

    Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman, and Karen Yorav. "Efficient Verification of Sequential and Concurrent C Programs." Formal Methods in System Design, Special Issue on Software Model Checking, Volume 25, Numbers 2-3, pages 129--166, September-November 2004.

  6. Modular Verification of Software Components in C

    Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith. "Modular Verification of Software Components in C. IEEE Transactions on Software Engineering, Volume 30, Number 6, pages 388--402, June 2004.

Conference and Workshop Papers

  1. From Scripts to Specifications: the Evolution of a Flight Software Testing Effort

    Alex Groce, Klaus Havelund, and Margaret Smith. "From Scripts to Specifications: the Evolution of a Flight Software Testing Effort." To appear in International Conference on Software Engineering (ICSE), 2010.

  2. (Quickly) Testing the Tester via Path Coverage

    Alex Groce. "(Quickly) Testing the Tester via Path Coverage." In Workshop on Dynamic Analysis (WODA), Chicago, Illinois, July 2009.

  3. Random Test Run Length and Effectiveness

    James H. Andrews, Alex Groce, Melissa Weston, and Ru-Gang Xu. "Random Test Run Length and Effectiveness." In IEEE/ACM Conference on Automated Software Engineering (ASE), pages 19--28, L'Aquila, Italy, September 2008.

  4. Tackling Large Verification Problems with the Swarm Tool*

    Gerard Holzmann, Rajeev Joshi, and Alex Groce. "Tackling Large Verification Problems with the Swarm Tool." In SPIN Workshop on Model Checking of Software (SPIN), pages 134--143, Los Angeles, California, August 2008.

  5. Automated Testing of Planning Models

    Klaus Havelund, Alex Groce, Gerard Holzmann, Rajeev Joshi, and Margaret Smith. "Automated Testing of Planning Models." In Workshop on Model Checking and Artificial Intelligence (MoChArt), Patras, Greece, July 2008.

  6. Random Testing and Model Checking: Building a Common Framework for Nondeterministic Exploration

    Alex Groce and Rajeev Joshi. "Random Testing and Model Checking: Building a Common Framework for Nondeterministic Exploration." In Workshop on Dynamic Analysis (WODA), pages 22--28, Seattle, Washington, July 2008.

  7. Extending Model Checking with Dynamic Analysis*

    Alex Groce and Rajeev Joshi. "Extending Model Checking with Dynamic Analysis." In Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), pages 142--156, San Francisco, California, January 2008.

  8. Verifying C++ with STL Containers via Predicate Abstraction

    Nicolas Blanc, Alex Groce, and Daniel Kroening. "Verifying C++ with STL Containers via Predicate Abstraction." In IEEE/ACM Conference on Automated Software Engineering (ASE), pages 521--524, Atlanta, Georgia, November 2007.

  9. Randomized Differential Testing as a Prelude to Formal Verification

    Alex Groce, Gerard Holzmann, and Rajeev Joshi. "Randomized Differential Testing as a Prelude to Formal Verification." In International Conference on Software Engineering (ICSE), pages 621--631, Minneapolis, Minnesota, May 2007.

  10. Exploiting Traces in Program Analysis*

    Alex Groce and Rajeev Joshi. "Exploiting Traces in Program Analysis." In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 379--393, Vienna, Austria, March-April 2006.

  11. Counterexample Guided Abstraction Refinement via Program Execution*

    Daniel Kroening, Alex Groce, and Edmund Clarke. "Counterexample Guided Abstraction Refinement via Program Execution." In International Conference on Formal Engineering Methods (ICFEM), pages 224--238, Seattle, Washington, November 2004.

  12. Explaining Abstract Counterexamples
    © ACM, 2004. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the ACM SIGSOFT 2004 International Symposium on the Foundations of Software Engineering, ACM SIGSOFT Software Engineering Notes Volume 29, Issue 6 (November 2004), http://doi.acm.org/10.1145/1029894.1029908.

    Sagar Chaki, Alex Groce, and Ofer Strichman. "Explaining Abstract Counterexamples." In Foundations of Software Engineering (SIGSOFT FSE), pages 73--82, Newport Beach, California, October-November 2004.

  13. Making the Most of BMC Counterexamples

    Alex Groce and Daniel Kroening. "Making the Most of BMC Counterexamples." In Workshop on Bounded Model Checking (BMC), pages 71--84, Boston, Massachusetts, July 2004.

  14. Understanding Counterexamples with explain*

    Alex Groce, Daniel Kroening, and Flavio Lerda. "Understanding Counterexamples with explain." In Computer Aided Verification (CAV), pages 453--456, Boston, Massachusetts, July 2004.

  15. Error Explanation with Distance Metrics*

    Alex Groce. "Error Explanation with Distance Metrics." In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 108--122, Barcelona, Spain, March-April 2004.

  16. VeriAgent: an Approach to Integrating UML and Formal Verification Tools

    E. Mota, E. Clarke, W. Oliveira, A. Groce, J. Kanda, and M. Falcao. "VeriAgent: an Approach to Integrating UML and Formal Verification Tools." In Sixth Brazilian Workshop on Formal Methods (WMF 2003), pages 111--129 (Elect. Notes Theor. Comput. Sci. 95), Universidade Federal de Campina Grande, Brazil, October 2003.

  17. Predicate Abstraction with Minimum Predicates*
    (Contains full versions of some tables that were cut for publication version.)

    Sagar Chaki, Edmund Clarke, Alex Groce, and Ofer Strichman. "Predicate Abstraction with Minimum Predicates." In Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), pages 19--34, L'Aquila, Italy, October 2003.

  18. What Went Wrong: Explaining Counterexamples*

    Alex Groce and Willem Visser. "What Went Wrong: Explaining Counterexamples." In SPIN Workshop on Model Checking of Software, pages 121--135, Portland, Oregon, May 2003.

  19. Modular Verification of Software Components in C

    Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith. "Modular Verification of Software Components in C." In International Conference on Software Engineering (ICSE), pages 385--395, Portland, Oregon, May 2003.
    (ICSE 2003 ACM SIGSOFT Distinguished Paper Award)

  20. AMC: An Adaptive Model Checker*

    Alex Groce, Doron Peled, and Mihalis Yannakakis. "AMC: An Adaptive Model Checker." In Computer Aided Verification (CAV), pages 521--525, Copenhagen, Denmark, July 2002.

  21. Model Checking Java Programs using Structural Heuristics
    © ACM, 2002. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis, ACM SIGSOFT Software Engineering Notes Volume 27, Issue 4 (July 2002), http://doi.acm.org/10.1145/566172.566175.

    Alex Groce and Willem Visser. "Model Checking Java Programs using Structural Heuristics." In International Symposium on Software Testing and Analysis (ISSTA), pages 12--21, Rome, Italy, July 2002.

  22. Heuristic Model Checking for Java Programs*

    Alex Groce and Willem Visser. "Heuristic Model Checking for Java Programs." In SPIN Workshop on Model Checking of Software, pages 242--245, Grenoble, France, April 2002.

  23. Adaptive Model Checking*

    Alex Groce, Doron Peled, and Mihalis Yannakakis. "Adaptive Model Checking." In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 357--370, Grenoble, France, April 2002.

  24. Efficient Model Checking Via Büchi Tableau Automata*

    Girish Bhat, Rance Cleaveland, and Alex Groce. "Efficient Model Checking Via Büchi Tableau Automata." In Computer Aided Verification (CAV), pages 38--52, Paris, France, July 2001.

*© Springer-Verlag
Final Springer version available at: Lecture Notes in Computer Science

Invited Papers

  1. Model Driven Code Checking

    Gerard Holzmann, Rajeev Joshi, and Alex Groce. "Model Driven Code Checking." In Automated Software Engineering, Special Issue on Trends in Automated Software Engineering, Volume 15, Number 3-4, pages 283--297, December 2008.

  2. Swarm Verification

    Gerard Holzmann, Rajeev Joshi, and Alex Groce. "Swarm Verification." In Conference on Automated Software Engineering (ASE), pages 1--6, L'Aquila, Italy, September 2008.

  3. Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving

    Alex Groce, Gerard Holzmann, Rajeev Joshi, and Ru-Gang Xu. "Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving." In Workshop on Constraints in Formal Verification, pages 1--15, Sydney, Australia, August 2008.

  4. New Challenges in Model Checking

    Gerard Holzmann, Rajeev Joshi, and Alex Groce. "New Challenges in Model Checking." In Symposium on 25 Years of Model Checking, Seattle, Washington, August 2006.

Technical Reports

  1. Verifying C++ with STL Containers via Predicate Abstraction

    Nicolas Blanc, Daniel Kroening, and Alex Groce. "Verifying C++ with STL Containers via Predicate Abstraction." Technical Reports 506, ETZ Zurich, January 2006.

  2. Error Explanation and Fault Localization with Distance Metrics

    Alex Groce. "Error Explanation and Fault Localization with Distance Metrics." Technical Report CMU-CS-05-121, Carnegie Mellon University, March 2005.

  3. What Went Wrong: Explaining Counterexamples [.ps.gz]

    Alex Groce and Willem Visser. "What Went Wrong: Explaining Counterexamples." Technical Report 02-08, RIACS, USRA, February 2002.

Back to Alex's Page
Comments & questions to agroce@gmail.com.