Faculty :: Marsha Chechik
Personal PagePublications
Interests: formal methods to improve quality and reliability of software, computer security.

Contact Information:

Students Supervised:

Courses Taught:

Projects Involved with:

    Service:

    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
    • M. Chechik and B. Devereux. ``Automated Support for Building Behavioural Models of Event-Driven Systems'', to appear in Automated Software Engineering (short paper), September, 2004
      PS PDF Abstract
    • M. Chechik and S. Uchitel. ``Merging Partial Behavioural Models'', in Proceedings of FSE'04, November, 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 D. Paun. ``On Closure Under Stuttering'', Formal Aspects of Computing, pp. 342-368, 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
    • M. Chechik and W. MacCaull. ``CTL Model-Checking Over Logics with Non-Classical Negations'', in Proceedings of 33rd IEEE International Conference on Multi-Valued Logics (ISMVL'03), pp. 293-300, May, 2003
      PS PDF Abstract
    • B. Devereux and M. Chechik. ``Edge-Shifted Decision Diagrams for Multi-Valued Logic'', Journal of Multi-Valued Logic and Soft Computing, vol. 9, pp. 59-86, 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
    2002:
    • M. Chechik and A. Wong. ``Formal Modeling in a Commercial Setting: A Case Study'', Journal of Systems and Software, vol. 60, pp. 57-80, January, 2002
      PS PDF Abstract
    • 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
    • M. Chechik and W. MacCaull. ``On Model-Checking over Logics with Non-Classical Negations'', CSRG Technical Report, Department of Computer Science, University of Toronto, October, 2002
      PS PDF Abstract
    • M. Chechik and W. Ding. ``Lightweight Reasoning About Program Correctness'', Information Systems Frontiers, vol. 4, pp. 363-377, November, 2002
      PS PDF Abstract
    • S. M. Easterbrook and M. Chechik. ``Guest Editorial: Special Issue on Model Checking in Requirements Engineering'', Requirements Engineering Journal, vol. 7, pp. 221-224, December, 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
    • Dimitrie O. Paun and Marsha Chechik. ``On Closure Under Stuttering'', Formal Aspects of Computing, 2002
      PS PDF Abstract
    2001:
    • M. Chechik, S. Easterbrook and V. Petrovykh. ``Model-Checking Over Multi-Valued Logics'', in Proceedings of Formal Methods Europe (FME'01), pp. 72-98, March, 2001
      PS PDF Abstract
    • M. Chechik, B. Devereux and S. Easterbrook. ``Implementing a Multi-Valued Symbolic Model-Checker'', in Proceedings of TACAS'01, pp. 404-419, April, 2001
      PS PDF Abstract
    • M. Chechik, B. Devereux, S. Easterbrook, A. Lai, and V. Petrovykh. ``Efficient Multiple-Valued Model-Checking Using Lattice Representations'', in Proceedings of 12th International Conference on Concurrency Theory (CONCUR'01), Aalborg, Denmark, pp. 451-465, August, 2001
      PS PDF Abstract
    • 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
    • M. Chechik and J. Gannon. ``Automatic Analysis of Consistency Between Requirements and Designs'', IEEE Transactions on Software Engineering, vol. 27, July, 2001
      PS PDF Abstract
    • M. Chechik and W. Ding. ``Lightweight Reasoning about Program Correctness'', in Proceedings of CASCON'01, Toronto, Canada, pp. 127-140, November, 2001
      PS PDF Abstract
    • M. Chechik and S. Easterbrook. ``Reasoning About Compositions of Concerns'', in Proceedings of Workshop on Advanced Separation of Concerns in Software Engineering, at the 23rd International Conference on Software Engineering (ICSE-01), Toronto, Canada, May, 2001
      PS PDF Abstract
    • S. Easterbrook and M. Chechik. ``A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints'', in Proceedings of International Conference on Software Engineering (ICSE'01), Toronto, Canada, pp. 411-420, May, 2001
      PS PDF Abstract
    • S. M. Easterbrook and M. Chechik. ``Automated Paraconsistent Reasoning via Model Checking'', in Proceedings of First International Workshop on Inconsistency in Data and Knowledge, at the International Joint Conference on Artificial Intelligence, (IJCAI-01), Seattle, USA, August, 2001
      PS PDF Abstract
    • S. M. Easterbrook and M. Chechik. ``A Framework to Handle Horizontal Inconsistency in Software'', in Proceedings of 2nd International Workshop on Living with Inconsistency, at the 23rd International Conference on Software Engineering (ICSE-01), Toronto, Canada, May, 2001
      PS PDF Abstract
    previous:
    • M. Chechik and H. Wang. ``Feasibility of Bisimulation Analysis of Protocols Expressed in SDL'', in Proceedings of CASCON'2000, November, 2000
      PS PDF Abstract
    • M. Chechik, William Andrepoulos, Bob Bernecky,Ariel Fuxman, Benet Devereux, Kristin Hofstee,Jingjing Lu, Tsuyoshi Morioka, Peeter Piegaze,Jeffrey Tang, Sean Thompson, Cosmin Truta,Yuxiang Zhu and Wei Zhou. ``Automated Verification, Fall 1999: A Collection of Reports'', CSRG Technical Report, Department of Computer Science, University of Toronto, 2000
      PS PDF Abstract
    • M. Chechik, S. Easterbrook, B. Devereux, A. Lai, V. Petrovykh and C. Thompson-Walsh. A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints -- Project Report, CSRG Technical Report, Department of Computer Science, University of Toronto, August, 2000
      PS PDF Abstract
    • M. Chechik and W. Ding. ``On Interpreting Results of Model-Checking with Abstraction'', CSRG Technical Report, Department of Computer Science, University of Toronto, December, 2000
      PS PDF Abstract
    • M. Chechik and D. Paun. Events in Property Patterns, in Proceedings of the 6th International SPIN Workshop (SPIN'6), pp. 154-167, September, 1999
      PS PDF Abstract
    • M. Chechik and A. Wong. ``Formal Methods When Money Is Tight'', in Proceedings of the First Workshop on Economics-Driven Software Engineering Research (EDSER-1), Los Angeles, May, 1999
      PS PDF Abstract
    • Dimitrie O. Paun and Marsha Chechik. ``Events in Linear-Time Properties'', in Proceedings of 4th International Conference on Requirements Engineering, June, 1999
      PS PDF Abstract
    • Andre Wong and Marsha Chechik. ``Formal Modeling in a Commercial Setting: A Case Study'', in Proceedings of FM'99: World Congress in Formal Methods, pp. 590-605, September, 1999
      PS PDF Abstract
    • M. Chechik. ``SC(R)^3: Towards Usability of Formal Methods'', in Proceedings of CASCON'98, pp. 177-191, November, 1998
      PS PDF Abstract
    • M. Chechik and V.S. Sudha. ``Checking Consistency between Source Code and Annotations'', CSRG Technical Report, Department of Computer Science, University of Toronto, 1998
      PS PDF Abstract
    • M. Chechik. ``Using SCR Requirements'', in Proceedings of the 7th SCR workshop, October, 1998
      PS PDF Abstract
    • M. Chechik and students of csc2108, Fall'97. ``Automated Verification: A Collection of Reports'', CSRG Technical Report, Department of Computer Science, University of Toronto, April, 1998
      PS PDF Abstract
    • Dimitrie O. Paun, Marsha Chechik, and Bernd Biechelle. ``Production Cell Revisited'', in Proceedings of the 4th International SPINWorkshop (SPIN'4), November, 1998
      PS PDF Abstract
    • Andre Wong and Marsha Chechik. ``Applying Formal Methods to a Telecommunications System in a Commercial Setting'', in Proceedings of 11th International Conference on Software Engineering and Its Applications, December, 1998
      PS PDF Abstract
    • M. Chechik. ``Checking Consistency Between Source Code and Annotations'', CSRG Technical Report, Department of Computer Science, University of Toronto, December, 1997
      PS PDF Abstract
    • M. Chechik. ``Software Engineering Education at the University of Toronto'', in Proceedings of the 4th Software Engineering Workshop, May, 1997
      PS PDF Abstract
    • D. Suydam and M. Chechik. ``Generating Test Cases from SCR Specifications'', CSRG Technical Report, Department of Computer Science, University of Toronto, 1997
      PS PDF Abstract
    • J. Atlee, M. Chechik and J. Gannon. ``Using Model Checking to Analyze Requirements and Designs'', Advances in Computers, 1996
      PS PDF Abstract
    • M. Chechik and J. Gannon. ``Verification of Consistency between Concurrent Program Designs and Their Requirements'', in Proceedings of COMPASS'96, Gaithersburg, Maryland, June, 1996
      PS PDF Abstract
    • M. Chechik. Automatic Analysis of Consistency between Requirements and Designs , PhD Thesis , University of Maryland, College Park, Maryland, December, 1996
      PS PDF Abstract
    • M. Chechik and J. Gannon. ``Automatic Analysis of Consistency Between Implementations and Requirements: A Case Study'', in Proceedings of 10th Annual Conference on ComputerAssurance, pp. 123-131, June, 1995
      PS PDF Abstract
    • M. Chechik and J. Gannon. ``Automatic Verification of Requirements Implementations'', in Proceedings of the 1994 International Symposiumon Software Testing and Analysis (ISSTA), Seattle, Washington, pp. 1-14, August, 1994
      PS PDF Abstract

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