PhD :: Arie Gurfinkel
Personal PagePublications
Interests: Automated reasoning about software systems, especially model-checking, and software engineering methodologies supporting it. Mathematical logic, automata theory, abstract interpretation, semantics of computation, lattice theory, reasoning with partial, incomplete, and inconsistent information, model exploration.

Contact Information:

PHD Thesis:
[ 2002 -- Current ] Model-Checking with Many Values
Advisors:

MSC Thesis:
[ 2000 -- 2002 ] Multivalued Model-checking: Counterexamples, Fairness and Running Time
Advisors:

Publications:


2006:
  • A. Gurfinkel and O. Wei and M. Chechik. ``Systematic Construction of Abstractions for Model-Checking'', in Proceedings of 7th International Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI'06), Charleston, SC, pp. 381--397, January, 2006
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``Why Waste a Perfectly Good Abstraction?'', in Proceedings of the 12th International Conference on Toolsand Algorithms for the Constructionand Analysis of Systems (TACAS'06), Vienna, Austria, March, 2006
    PS PDF Abstract
2005:
  • M. Chechik and A. Gurfinkel. ``A Framework for Counterexample Generation and Exploration'', in Proceedings of Fundamental Approaches toSoftware Engineering (FASE'05), Edinburgh, Scotland, pp. 217--233, April, 2005
    PS PDF Abstract
  • M. Chechik and A. Gurfinkel. ``A Framework for Counterexample Generation and Exploration'', Submitted to International Journal on Software Toolsfor Technology Transfer, September, 2005
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``How Thorough is Thorough Enough'', in Proceedings of 13th Advanced Research WorkingConference on Correct Hardware Design andVerification Methods (CHARME'05), Saarbr\"{u}cken, Germany, pp. 65--80, October, 2005
    PS PDF Abstract
  • S. Nejati and A. Gurfinkel and M. Chechik. ``Stuttering Abstraction for Model Checking'', in Proceedings of 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, pp. 311--320, September, 2005
    PS PDF Abstract
  • O. Wei and A. Gurfinkel and M. Chechik. ``Identification and Counter Abstraction for Full Virtual Symmetry'', in Proceedings of 13th Advanced Research WorkingConference on Correct Hardware Design andVerification Methods (CHARME'05), Saarbr\"{u}cken, Germany, pp. 285--300, October, 2005
    PS PDF Abstract
2004:
  • M. Chechik, S. Berezin, C. Barrett, I. Shikanian, A. Gurfinkel, and D. Dill. ``A Practical Approach to Partial Functions in CVC Lite'', in Proceedings of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, July, 2004
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``How Vacuous Is Vacuous?'', in Proceedings of 10th International Conference on Toolsand Algorithms for the Construction and Analysis ofSystems (TACAS'04), Barcelona, Spain, pp. 451--466, March, 2004
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``Extending Extended Vacuity'', in Proceedings of 5th International Conference onFormal Methods in Computer-Aided Design (FMCAD'04), Austin, Texas, pp. 306--321, November, 2004
    PS PDF Abstract
2003:
  • M. Chechik, Benet Devereux, Arie Gurfinkel, and Steve Easterbrook. ``Multi-Valued Symbolic Model-Checking'', ACM Transactions on Software Engineering and Methodology, vol. 12, pp. 1-38, October, 2003
    PS PDF Abstract
  • M. Chechik and A. Gurfinkel. ``TLQSolver: A Temporal Logic Query Checker'', in Proceedings of 15th International Conference on Computer Aided Verification (CAV'03), pp. 210-214, July, 2003
    PS PDF Abstract
  • S. M. Easterbrook, M. Chechik, B. Devereux, A. Gurfinkel, A. Lai, V. Petrovykh, A. Tafliovich, and C. Thompson-Walsh. ``XChek: A Model Checker for Multi-Valued Reasoning'', in Proceedings, 25th International Conference on Software Engineering, Portland, Oregon, May, 2003
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``Proof-like Counterexamples'', in Proceedings of 9th International Conference on Toolsand Algorithms for the Construction and Analysis ofSystems (TACAS'03), Warsaw, Poland, pp. 160--175, April, 2003
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``Multi-Valued Model-Checking via ClassicalModel-Checking'', in Proceedings of 14th International Conferenceon Concurrency Theory (CONCUR'03), Marseille, France, pp. 263-277, September, 2003
    PS PDF Abstract
  • A. Gurfinkel, M. Chechik, and B. Devereux. ``Temporal Logic Query Checking: A Tool for Model Exploration'', IEEE Transactions on Software Engineering, vol. 29, pp. 898-914, October, 2003
    PS PDF Abstract
  • A. Gurfinkel and M. Chechik. ``Generating Counterexamples for Multi-Valued Model-Checking'', in Proceedings of Formal Methods Europe (FME'03), Pisa, Italy, pp. 503--521, September, 2003
    PS PDF Abstract
  • S. Nejati and A. Gurfinkel. ``Stuttering Refinement on Partial Systems'', in Proceedings of the Eighteenth Annual IEEE Symp.on Logic in Computer Science (LICS'03), Short Paper, June, 2003
    PS PDF Abstract
2002:
  • M. Chechik, B. Devereux and A. Gurfinkel. ``XChek: A Multi-Valued Model-Checker'', in Proceedings of 14th International Conference on Computer-Aided Verification (CAV'02), Copenhagen, Denmark, pp. 505-509, July, 2002
    PS PDF Abstract
  • M. Chechik, A. Gurfinkel, B. Devereux, A. Lai, and S. Easterbrook. ``Data Structures for Symbolic Multi-Valued Model-Checking'', CSRG Technical Report, Department of Computer Science, University of Toronto, January, 2002
    PS PDF Abstract
  • A. Gurfinkel and B. Devereux and M. Chechik. ``Model Exploration with Temporal Logic Query Checking'', in Proceedings of SIGSOFT Conference on Foundationsof Software Engineering (FSE'02), Charleston, SC, pp. 139--148, November, 2002
    PS PDF Abstract
  • A. Gurfinkel. Multi-Valued Symbolic Model-Checking:Fairness, Counter-Examples, Running Time , Master Thesis, Department of Computer Science, University of Toronto, Toronto, Ontario, Canada, October, 2002
    PS PDF Abstract
2001:
  • M. Chechik, B. Devereux and A. Gurfinkel. ``Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN'', in Proceedings of the 8th SPIN Workshop on Model Checking Software, Toronto, Canada, pp. 16-36, May, 2001
    PS PDF Abstract

For questions and suggestions contact the webmaster
Formal Methods Group, CS Department, University of Toronto 2004