Home Schedule Model Database Paper Calls People Research

Conference Papers

N. Rungta and E. G. Mercer. "Guided model checking for programs with polymorphism," ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), Savannah, January 2009.

N. Rungta and E. G. Mercer. "A meta heuristic for effectively detecting concurrency errors," Haifa Verification Conference, Haifa, Israel, November 2008.

R. Kumar and E. G. Mercer. "Verifying Communication Protocols Using Live Sequence Chart Specifications," Eigth International Workshop on Automated Verification of Critical Systems, Glasgow, UK, pp. 31 - 45, September 2008.

R. Kumar and E. G. Mercer. "Improving Live Sequence Chart to Automata Translation for Verification," Seventh International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), Budapest, Hungary, pp. 51 - 64, March 2008.

N. Rungta, H. Carroll, E. G. Mercer, R. J. Roper, M. Clement and Q. Snell. "Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs," Formal Methods in Computer Aided Design (FMCAD '07), Austin, USA, November 2007.

N. Rungta and E. G. Mercer. "Hardness for Explicit State Software Model Checking Benchmarks," 5th IEEE International Conference on Software Engineering and Formal Methods, London, U.K, September 2007.

R. Kumar, E. G. Mercer and A. Bunker. "Improving Translation of Live Sequence Charts to Temporal Logic," Seventh International Workshop on Automated Verification of Critical Systems, Oxford, U.K, September 2007.

N. Rungta and E. G. Mercer. "Generating Counter-examples through Randomized Guided Search," SPIN Workshop on Model Checking of Software, Berlin, Germany, July 2007.

J. Self and E. G. Mercer. "On-the-fly Dynamic Dead Variable Analysis," SPIN Workshop on Model Checking of Software, Berlin, Germany, July 2007.

N. Rungta and E. G. Mercer. "An improved distance heuristic function for directed software model checking," Formal Methods in Computer Aided Design (FMCAD '06), San Jose, USA, November 2006.

M. Lewis and M. D. Jones. "A Dead Variable Analysis for Explicit Model Checking," ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM '06), Charleston, South Carolina, January 2006.

N. Rungta and E. G. Mercer. "A Context-sensitive Structural Heuristic for Guided Search Model Checking," 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, USA, November 2005.

E. G. Mercer and M. D. Jones. "Model Checking Machine Code with the GNU Debugger," SPIN Workshop on Model Checking of Software, San Francisco, USA, August 2005.

T. Bao and M. D. Jones. "Time-efficient Model Checking with Magnetic Disk," Tools and Algorithms for the Construction and Analysis of Systems (TACAS05), Nicolas Halbwachs and Lenore D. Zuck, Springer, Edinburgh, Scotland, no. 3440, in LNCS, pp. 526-540, April 2005.

M. D. Jones, D. Delorey and A. Benson. "Using Refinement to Show Compatibility," Theorem Provers in Higher Order Logics (TPHOLs'04), K. Slind, A. Bunker and G. Gopalakrishnan, Park City, Utah, no. 3223, in LNCS, September 2004.

R. Kumar and E. G. Mercer. "Load Balancing Parallel Explicit State Model Checking," Parallel and Distributed Model Checking, London, UK, August 2004.

K. Seppi, M. Jones and P. Lamborn. "Guided Model Checking with a Bayesian Meta-heuristic," Applications of Concurrency to System Design (ACSD'04)--The experimental results in this paper are significantly incorrect. A corrected version will appear in Fundamentae Informatica, Hamilton, Ontario, Canada, June 2004.

M. D. Jones and E. Mercer. "Explicit state model checking with Hopper," International SPIN Workshop on Software Model Checking (SPIN'04), Springer, Barcelona, Spain, no. 2989, in LNCS, pp. 146-150, March 2004.

M. D. Jones, E. G. Mercer, T. Bao and R. Kumar and P. Lamborn. "Benchmarking Explicit State Parallel Model Checkers," Parallel and Distributed Model Checking, Boulder, Colorado, July 2003.

A. Weinzoepflen, M. Jones, D. Mery and D. Cansell and G. Gopalakrishnan. " Incremental construction of a proof the producer/consumer property for the PCI protocol," The Second International Z and B Conference, January 2002.

Michael Jones and Ganesh Gopalakrishnan. "Verifying transaction ordering properties in unbounded bus networks through combined deductive/algorithmic methods," Formal Methods in Computer-Aided Design: FMCAD'00, Warren A. Hunt Jr. and Steven D. Johnson, Austin, Texas, no. 1954, in LNCS, pp. 505-519, November 2000, A proof about transaction ordering that includes a manualy derrived and validated abstraction with a manual transaction to the Murφ model checler.

Annette Bunker, Michael D. Jones and Trent N. Larson and Phillip J. Windley. "Alexandria: Libraries of Abstract," 2nd Workshop on Libraries, Toledo, Spain, April 1997.

Paul E. Black, Kelly M. Hall, Michael D. Jones, Trent N. Larson and Phillip J. Windley. "A Brief Introduction to Formal Methods," Proceedings of the IEEE 1996 Custom Integrated Circuits Conference, May 1996, An overview of various approaches to formal verification of hardware including theorem proving and model checking. Theorem proving is more concise and useful in applications where abstraction is important while model-checking is less abstract but requires very little user-intervention.

Journal Articles

Michael Jones and Jacob Sorber. "Parallel Search for LTL Violations," in Software Tools for Technology Transfer (STTT). vol. 7, no. 1, pp. 31-42, 2005.

Kevin Seppi, Michael Jones and Peter Lamborn. "Guided Model Checking with a Bayesian Meta-Heuristic," in Fundamenta Informaticae. 2005, To appear. This article corrects significant errors in the results of the ACSD 2004 paper with the same title.

Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones and Ganesh Gopalakrishnan. "Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem," in Formal Methods in Systems Design. vol. 16, no. 1, pp. 93-119, January 2000.

M.S. Theses

Joel Self. On-the-fly Dynamic Dead Variable Analysis, Brigham Young University, 2007.

Dritan Kudra. Finding Termination and Time Improvement in Predicate Abstraction with Under-Approximation and Abstract Matching, Brigham Young University, 2007.

Joseph R. Edelman. Machine Code Verification using the Bogor Framework, Brigham Young University, 2007.

Neha Rungta. Improving Error Discovery Using Guided Model Checking, Brigham Young University, 2006.

Rahul Kumar. Load Balancing Parallel and Explicit State Model Checking, Brigham Young University, 2004.

Ph.D. Theses

Rahul Kumar. Using Live Sequence Chart Specifications for Formal Verification of Systems. Brigham Young University, 2008.

Miscellaneous

T. Bao and M. Jones. TR SMC-BYU-0109: Refinement for Predicate Abstraction in the Context of Abstract Component Model, Dept. of Computer Science, 2008.

N. Rungta and E. G. Mercer. TR SMC-BYU-0110: A distance heuristic for polymorphic programs, Dept. of Computer Science, 2008.

N. Rungta and E. G. Mercer. TR SMC-BYU-0108: Guided Test for detecting concurrency errors, Dept. of Computer Science, 2008.

N. Rungta and E. G. Mercer. TR SMC-BYU-0107: Hardness for Explicit State Software Model Checking Benchmarks, Dept. of Computer Science, 2007.

N. Rungta and E. G. Mercer. A Context-sensitive Structural Heuristic for Guided Search Model Checking, Dept. of Computer Science, 2005.

M. Lewis. TR SMC-BYU-0105: Interrupt Handlers in Dead Variable Analysis, Dept. of Computer Science, 2005.

R. Kumar, M. D. Jones and E. G. Mercer. Dynamic Partition Algorithm for Distributed Murphi, Dept. of Computer Science, 2004.

T. Bao. TR VV-0402: Empirical Comparison of Algorithms for Model Checking with Magnetic Disk, Dept. of Computer Science, 2004.

K. Seppi, M. Jones and P. Lamborn. Guided Model Checking with a Bayesian Meta-heuristic, Dept. of Computer Science, 2004.

K. Seppi. TR VV-0301: Empirical Bayes Assisted Probabilistic Search, Dept. of Computer Science, 2003.

Validation and Verification • 3325 Talmage • Brigham Young University • Provo UT

Disclaimer