Publications
2011
- M. Chechik, S. Nejati, M. Sabetzadeh. ``A Relationship-Based Approach to Model Integration'', 16 pages, submitted in January 2011. [PDF]
- A. Gurfinkel, M. Chechik. ``Robust Vacuity for Branching
Temporal Logic''. Journal version of the FMCAD'04 paper. To appear in
ACM Transactions on Computational Logic, 2011. 36 pages. [PDF]
- O. Wei, A. Gurfinkel, M. Chechik.
``On the Consistency, Expressiveness, and Precision of Partial Models''. Journal version of the VMCAI'09
paper. Journal of Information and Computation, 209(1), pp. 20-47,
2011. [PDF]
- G. Brunet, M. Chechik, D. Fischbein, N. D'Ippolito, S. Uchitel.
``Weak Alphabet Merging of Partial Behaviour Models''. To appear in
ACM Transactions on Software Engineering and Methodology,
53 pages, 2011. [PDF]
2010
- M. Chechik and J. Simmonds and S. Ben-David and S. Nejati and M. Sabetzadeh and
R. Salay.
``Modeling and Analysis of Personal Web Applications: A Vision''. In Proceedings of
NSERC/CASCON Symposium on Personal Web, November 2010. [PDF]
- M. Chechik and A. Gurfinkel and S. Uchitel and S. Ben-David. ``Raising Level of Abstraction with Partial Models: A Vision''. In Proceedings of NSF/MSR Workshop
on Usable Verification, November 2010. [PDF]
-
Jocelyn Simmonds. Dynamic Analysis of Web Services. Ph.D. Thesis, University of Toronto, 2010. [PDF]
- F. van Breugel, M. Chechik, "19th International Conference
on Concurrency Theory: Selection of Best Papers".
Journal of Information and Computation, 208(10), pp. 1091-1092,
2010.
- J. Simmonds, J. Davies, A. Gurfinkel, M. Chechik.
``Exploring Resolution Proofs to Speed Up LTL Vacuity Detection for BMC''.
Journal version of the FMCAD'07 paper.
Springer International Journal of Software Tools for Technology
Transfer (STTT), Volume 12, Number 5, pp. 319-335, January 2010.
[PDF]
- M. Chechik, S. Uchitel, M. Sassolas.
``Exploring Inconsistencies between Modal Transition Systems''.
J. of Software and System Modeling (SoSyM), 41 pages, 2010. [PDF]
Published online February 2010.
- Michail Famelis. Relationship-Driven Model Management,
Masters Thesis, April 2010. [PDF]
- Aws Albarghouthi, Abstract Analysis of
Symbolic Executions, Masters Thesis, January 2010. [PDF]
- J. Simmonds, S. Ben-David, M. Chechik. ``Monitoring and Recovery of
Web Service Applications''. Book chapter in Smart Internet
Technologies, J. Cordy, M. Chignell, J. Ng, eds., April 2010. 40 pages. [PDF]
- S. Nejati, M. Sabetzadeh, M. Chechik, S. Easterbrook, P. Zave. ``Matching and Merging of Variant Feature Specifications''. Journal version of the ICSE'07 paper.
Submitted in September 2010, 22 pages. [PDF]
- J. Simmonds, S. Ben-David, M. Chechik. ``Guided Recovery for Web Service
Applications''. 15 pages. In
Proceedings of Foundations of Software Engineering (FSE'10),
November 2010. [PDF]
- A. Albarghouthi, A. Gurfinkel, O. Wei, M. Chechik. ``Abstract
Analysis of Symbolic Executions''. In
Proceedings of International Conference on Computer-Aided
Verification, Lecture Notes in Computer
Science, Volume 6174, pages 495-510, July 2010. Springer. [PDF]
- M. Famelis, R. Salay, M. Chechik, Q. Zhu, R. Baillargeon.
``Managing Heterogeneous Model Relations with MMTF''. 6 pages, submitted
- M. Chechik, R. Salay, M. Famelis, S. Ben-David, O. Ogunbiyi.
``Using partial models to support change propagation: A position
paper''. 16 pages, July 2010. Submitted.
- J. Simmonds, M. Chechik. ``RUMOR: Monitoring and
Recovery of BPEL Applications''.
In Proceedings of International Conference on Automated Software
Engineering, September 2010, pages 345-346. Tools paper. [PDF]
- J. Simmonds, S. Ben-David, M. Chechik.
``Optimizing Computation of Recovery Plans for BPEL Applications''.
In Proceedings of ASE'10 Workshop on Testing and Verification
of Web Systems, EPTCS Volume 35, pp. 3-14, September 2010. [PDF]
- M. Sabetzadeh, S. Nejati, M. Chechik, and S. Easterbrook. ``Reasoning about Consistency in Model Merging''. In Proceedings of 3rd Workshop on Living With Inconsistency in Software Development, 6 pages, September 2010. [PDF]
- J. Rubin, M. Chechik. ``From Products to Product Lines Using Model
Matching and Refactoring''. In Proceedings of 2nd International
Workshop on Model-Driven Software Product Line Engineering (MAPLE'2010),
6 pages, September 2010. [PDF]
2009
-
Ou Wei. Abstraction for Verification and Refutation in
Model Checking. Ph.D. Thesis, University of Toronto, 2009. [PDF]
-
Mihaela Bobaru (Gheorghiu). Approximation and Refinement Techniques for Hard Model-Checking Problems.
Ph. D. Thesis, University of Toronto, 2009. [PDF]
-
with F. Torshizi, J. Ostroff, R. Paige. ``The SCOOP Concurrency Model in Java-like Languages''. In Proceedings of CPA'09,
November 2009, pages 7-27 [PDF]
-
Winnie Lai. Relationship-Based Change Propagation: A Case Study . M.Sc. thesis, University of Toronto, April 2009. [PDF]
-
with J. Simmonds, Y. Gan, S. Nejati, B. O'Farrell, E. Litani, J. Waterhouse.
``Runtime Monitoring of Web Service Conversations''. In
IEEE Transactions on Service Computing, 2(3), pages 223-244, 2009. [PDF]
-
with W. Lai, S. Nejati, J. Cabot, Z. Diskin, S. Easterbrook, M. Sabetzadeh,
R. Salay. ``Relationship-Based Change Propagation: A Case Study''.
In Proceedings of ICSE'09 Workshop on Modeling in Software Engineering (MiSE'09), May 2009. [PDF]
-
with Ou Wei and Arie Gurfinkel.
``Mixed Transition Systems Revisited''. In
Proceedings of VMCAI'09, January 2009, 13 pages.
[PDF].
- with Sebastian Uchitel and Greg Brunet. ``Behavioural Model Synthesis
from Properties and Scenarios''. IEEE Transactions
on Software Engineering, 35(3), pages 384-406, 2009. [PDF]
-
T. Hart, K. Ku, A. Gurfinkel, M. Chechik, D. Lie. ``Augmenting Counterexample-Guided Abstraction Refinement with Proof
Templates''. Submitted.
- M. Chechik. ``How Smart are Your Services (Reasoning about Correctness of Web Services)'',
in Proceedings of CAS/NSERC Strategic Workshop on Smart Internet Technologies, November 2009. [PDF]
- M. Chechik. ``A relationship-based approach to model management''. In
Proceedings of MOMPES'09, p. 1 (invited) [PDF]
2008
-
Shiva Nejati. Behavioural Model Fusion. Ph.D. thesis,
University of Toronto, September 2008. [PDF]
-
with Arie Gurfinkel and Ou Wei. "Model Checking Reachability and
Non-Termination of Recursive Programs".
In Proceedings of 6th International Symposium on
Automated Technology for Verification (ATVA'08)
October 2008.
[PDF]
-
with Tom Hart and David Lie.
``Security Benchmarking using Partial Verification''. In
Proceedings of 3rd USENIX Workshop on Hot Topics in Security
(HotSec'08), July 2008. 6 pages.
-
with Tom Hart, Kelvin Ku, David Lie, Arie Gurfinkel.
``Augmenting Counterexample-Guided Abstraction Refinement with
Proof Templates''. In Proceedings of International
Conference on Automated Software Engineering (ASE'08) (short paper),
September 2008. 4 pages. [PDF]
-
with N. D'Ippolito, D. Fishbein and S. Uchitel.
``MTSA: The Modal Transition System Analyzer.'',
2 pages. In Proceedings of International Conference
on Automated Software Engineering (ASE'08), September 2008. Tools paper.
[PDF]
-
with T. Hart, K. Ku, A. Gurfinkel and D. Lie.
``PTYasm: Software Model Checking with Proof Templates'', 2 pages.
In Proceedings of International Conference
on Automated Software Engineering (ASE'08), September 2008. Tools paper.
[PDF]
-
Kelvin Ku. ``Software Model-Checking: Benchmarking and Techniques
for Buffer Overflow Analysis''. University of Toronto M.Sc. thesis,
January 2008. [PDF]
-
with S. Nejati, M. Sabetzadeh, S. Uchitel and P. Zave.
``Towards Compositional Synthesis of Evolving Systems''.
In Proceedings of FSE'08, November 2008, 11 pages. [PDF]
- with Arie Gurfinkel.
``Robust Vacuity for Branching Temporal Logic''.
Submitted for publication, March 2008, 27 pages. Accepted in July, 2008
pending revisions. Submitted for rereview in October 2008.
- with Shiva Nejati. ``Behavioural Model Fusion: Experiences from
Two Telecommunication Case Studies''. In Proceedings
of ICSE'08 Workshop on Modeling in Software Engineering (MiSE'08),
May 2008. [PDF]
- with Julia Rubin and Steve Easterbrook. ``A Declarative Approach
for Model Composition''. In Proceedings of
ICSE'08 Workshop on Modeling in Software Engineering (MiSE'08),
May 2008. [PDF]
-
with Jocelyn Simmonds and Shiva Nejati. ``Property Patterns for Runtime Monitoring of Web Service
Conversations'', 18 pages. In Proceedings of
Runtime Verification, March 2008 [PDF].
-
with M. Sabetzadeh, S. Nejati, S. Easterbrook. ``Global Consistency
Checking of Distributed Models with TreMer+''. Formal demo. In
Proceedings of ICSE'08, May 2008. 4 pages.
[PDF]
2007
-
with R. Salay, S. Easterbrook, Z. Diskin,
S. Nejati, M. Sabetzadeh, P. McCormick, P. Viriyakattiyaporn.
``An Eclipse-Based Model Management Framework''.
In Proceedings of OOPSLA'07 Workshop on Eclipse Technology,
November 2007. 6 pages [PDF].
-
Yuan Gan. ``Runtime Monitoring of Web Service Conversations''. M.Sc.
thesis, University of Toronto, March 2007. [PDF]
-
with Kevin Ku, Tom Hart, David Lie. ``A Buffer Overflow Benchmark For Software
Model Checkers''. In Proceedings of ASE'07. November 2007. [PDF]
-
with Jocelyn Simmonds, Jessica Davies, Arie Gurfinel. ``Exploiting
Resolution Proofs to Speed up LTL Vacuity Detection for BMC''.
In Proceedings of FMCAD'07, November 2007.
[PDF].
Journal version submitted for publication in October 2008.
-
with Yuan Gan, Shiva Nejati, Jon Bennett, Bill O'Farrell, Julie Waterhouse.
"Runtime Monitoring of Web Service Compositions". In
Proceedings of CASCON'07, November 2007. 16 pages. [PDF] Winner of Best Student Paper Award.
-
with Mahrdad Sabetzadeh, Shiva Nejati, Satirios Liaskos and Steve
Easterbrook. "Consistency Checking of Conceptual Models via
Model Merging". In Proceedings of IEEE International
Conference on Requirements Engineering (RE'07), October
2007, 15 pages. [PDF]
-
with Arie Gurfinkel. "A Framework for Counterexample Generation
and Exploration" (journal version of FASE'05 paper). In
Software Tools for Technology Transfer (STTT), Vol. 9,
No. 5-6, pp. 429-445, October 2007. [postscript]
-
with Mihaela Gheorghiu and Arie Gurfinkel. "Finding State Solutions to
Temporal Queries". In Proceedings of Integrated
Formal Methods (IFM'07), July 2007. LNCS 4591, pp. 273-292. [PDF]
-
with Shiva Nejati, Mehrdad Sabetzadeh and Steve Easterbrook.
"A Relationship-Driven Approach to Model Merging". In
Proceedings of ICSE 2007 Workshop on Models in Software Engineering
(MiSE'07), May 2007. [PDF]
-
with Sebastian Uchitel, Greg Brunet and Dario Fischbain.
"Partial Behavioural Models for Requirements and Early
Design". In Proceedings of 2006 Dagstuhl Seminar
on Methods for Modelling Software Systems (MMOSS), LNCS, 2007.
[PDF].
-
with Mihaela Gheorghiu and Arie Gurfinkel. "Finding Environmental Guarantees".
In Proceedings of FASE'07, LNCS 4422, March-April 2007.
[abstract] [PDF].
-
with Shiva Nejati, Mehrdad Sabetzadeh, Steve Easterbrook and Pamela Zave.
"Matching and Merging of Statecharts Specifications".
In Proceedings of ICSE'07, May 2007. [pdf]
Winner of Distinguished Paper Award
-
with Sebastian Uchitel and Greg Brunet.
"Behaviour Model Synthesis From Properties and Scenarios".
In Proceedings of ICSE'07, May 2007. [pdf]
2006
-
with Merhrad Sabetzadeh, Shiva Nejati and Steve Easterbrook. "A Relationship-Driven Approach to
View Merging", in Posters track, SIGSOFT FSE'06, 3 pages, November 2006.
-
with Mihaela Gheorghiu and Arie Gurfinkel. "VaqUoT: A Tool for Vacuity Detection", in Tools and Posters track of Formal Methods 2006, 4 pages,
August 2006. [PDF]
-
with Mihaela Gheorghiu and Arie Gurfinkel. "TLQ: A Query Solver for States", in Tools and Posters track of Formal Methods 2006, 4 pages,
August 2006. [PDF]
-
with Jocelyn Simmonds, Jessica Davies and Arie Gurfinkel. "VaqTree:
Efficient Vacuity Detection for Bounded Model Checking",
in Tools and Posters track of Formal Methods 2006, 4 pages,
August 2006. [PDF]
-
with Mehrdad Sabetzadeh, Shiva Nejati, and Steve Easterbrook.
"TReMer: A Tool for Relationship-Driven Model Merging".
in Tools and Posters track of Formal Methods 2006, 3 pages,
August 2006. [PDF]
-
with Shiva Nejati, Mehrdad Sabetzadeh, Steve Easterbrook.
"Identifying and Representing Requirements Variability in
Families of Reactive Software". CS Technical Report, February 2006.
-
with Greg Brunet and Sebastian Uchitel. "Generating Unbiased
Models from Temporal Properties". CS Technical Report, April 2006.
- with Greg Brunet and Sebastian Uchitel. "Merging Partial Behavioural
Models". Submitted for publication, May 2006. 50 pages.
-
with Greg Brunet and Sebastian Uchitel.
"Properties of Behavioural Model Merging", in Proceedings of
Formal Methods (FM'06), LNCS 4085, pp. 98-114, August 2006. [abstract] [PDF].
-
with Arie Gurfinkel, Benet Devereux, Albert Lai and Steve Easterbrook, "Data Structures for
Symbolic Multi-Valued Model-Checking", Formal Methods in
Software Design, 29(3), pp. 295-344..
[abstract]
[PDF],
- with Greg Brunet, Steve Easterbrook, Shiva Nejati,
Nan Niu and Marhdad Sabetzadeh. "A Manifesto for Model Merging",
in 1st International Workshop on Global Integrated
Model Management (ICSE'06 workshop), May 2006 [postscript].
-
with Shiva Nejati and Mihaela Gheorghiu. "Thorough Checking Revisited".
In Proceedings of Formal Methods in
Computer Aided Design (FMCAD'06), November 2006. [abstract] [PDF]
- with Arie Gurfinkel and Ou Wei. "Yasm: A Software Model-Checker
for Verification and Refutation", in Proceedings of CAV'06, LNCS 4144, pp. 170-174, August 2006. [postscript]
- with Arie Gurfinkel and Ou Wei.
"Systematic Construction of Abstractions for Model-Checking".
In Proceedings of VMCAI'06, LNCS 3855, pp. 381-397, January 2006. [abstract] [PDF]
-
with Benet Devereux. "Automated Support for Building Behavioural Models
of Event-Driven Systems", in Proceedings of
FASE'06, LNCS 3922, pp. 122-138, April 2006.
[postscript]
-
with Arie Gurfinkel. "Why Waste a Perfectly Good Abstraction?",
in Proceedings of TACAS'06, LNCS 3920, pp. 212-226, April 2006.
[postscript]
2005
- with Arie Gurfinkel. "A Framework for Counterexample
Generation and Exploration", LNCS 3442, pp. 217-233, Proceedings of FASE'05, Edinburgh, UK, April 2005.
[abstract] [postscript]
-
with Shiva Nejati and Arie Gurfinkel. "Stuttering Abstraction
for Model Checking", in Software Engineering
and Formal Methods (SEFM'05), September 2005. [abstract] [postscript]
-
with Ou Wei and Arie Gurfinkel. "Identification and Counter Abstraction for Full Virtual Symmetry", in CHARME'05, October 2005. [abstract] [postscript]
-
with Arie Gurfinkel. "Model-Checking Software Using Precise Abstractions", in IFIP WC on Verified Software: Tools, Techniques, and Experiments, October 2005. [postscript]
2004
-
Benet Devereux and Arie Gurfinkel. "Irrelevance and Vacuity in SAT-Based
Model-Checking". University of Toronto Technical Report. May 2004.
[ps]
-
with Benet Devereux, Arie Gurfinkel and Steve Easterbrook, "Multi-Valued Symbolic Model-Checking".
ACM Transactions on Software Engineering
and Methodology, Vol. 12, No. 4, October 2003, pages 1-38.
[abstract] [PDF].
-
with Sergey Berezin, Clark Barrett, Igor Shikanian, Arie Gurfinkel and David Dill.
"Logic with Partial Functions in CVC Lite", in
Proceedings of 2nd Workshop on Pragmatics of Decision Procedures in
Automated Reasoning, July 2004.
[abstract] [postscript].
-
with Sebastian Uchitel. "Merging Partial Behavioural Models",
in Proceedings of FSE'04, November 2004.
[abstract] [postscript].
-
with Arie Gurfinkel. "Extending Extended Vacuity", in
Proceedings of FMCAD'04, LNCS 3312, November 2004.
[abstract] [postscript]
-
with Arie Gurfinkel. "How Vacuous is Vacuous?", in
Proceedings of TACAS'04, March 2004, LNCS Vol. 2988, pp. 451-466,
Springer.
[abstract] [postscript].
2003
-
with Arie Gurfinkel, "Proof-Like Counter-Examples",
in Proceedings of TACAS'03, LNCS 2619, pp. 160-175, April 2003, Springer.
[abstract] [postscript]
-
with Arie Gurfinkel, "Multi-Valued Model Checking via Classical Model Checking". In Proceedings of CONCUR'03 , LNCS 2761, September 2003.
[abstract] [postscript]
-
with Arie Gurfinkel, "Generating Counterexamples for Multi-Valued Model-Checking". In Proceedings of Formal Methods Europe (FME'03), LNCS 2805, September 2003.
[abstract] [postscript]
-
with Arie Gurfinkel and Benet Devereux. "Temporal Logic Query Checking: A Tool
for Model Exploration". March 2003, updated July 2003. IEEE Transactions
on Software Engineering, Vol. 29, No. 10, pp. 898-914, October 2003.
[abstract] [postscript]
-
with Steve Easterbook, Benet Devereux, Arie Gurfinkel, Albert Lai, Chrostopher Thompson-Walsh, Anya Tefliovich,
Victor Petrovykh. "XChek: A Model-Checker for Multi-Valued Reasoning". In
Proceedings of ICSE'03, May 2003. [PDF-Long]
[PDF-Short]
-
with Dimitrie Paun, "On Closure Under Stuttering",
Formal Aspects of Computing, volume 14, pp. 342-368, 2003.[abstract] [postscript] Also
available as CSRG Technical Report 394.
-
with Benet Devereux, "Edge-Shifted Decision Diagrams for Multiple-Valued
Logic", in Journal of Multi-Valued Logic and Soft Computing,
vol. 9, no. 1, pp. 59-86, Old City Publishing Inc., 2003.
[abstract] [postscript].
Also available as CSRG Technical Report 444.
-
with Arie Gurfinkel, "TLQSolver: A Temporal Logic Query Checker". In Proceedings of 15th International Conference on Computer Aided Verification (CAV'03), LNCS 2725, pp. 210-214,
July 2003. [postscript].
-
with Wendy MacCaull, "CTL Model-Checking Over Logics with Non-Classical Negations". In Proceedings of 33rd IEEE International Conference on Multi-Valued
Logics (ISMVL'03), May 2003, pp. 293-300.
[abstract] [postscript]
2002
-
Arie Gurfinkel. Multi-Valued Symbolic Model-Checking: Fairness, Counterexamples, Running Time. University of Toronto MS Thesis, 2002.
[postscript]
-
with Steve Easterbrook, "Guest Editorial: Special Issue on Model Checking in Requirements Engineering". In Requirements Engineering, Volume 7,
issue 4, pp. 221-224, 2002. Springer-Verlag. [PDF].
-
with Arie Gurfinkel and Benet Devereux, "Model Exploration with Temporal Logic Query Checking",
in Proceedings of SIGSOFT Conference on Foundations of Software Engineering (FSE'02),
November 2002, pp. 139-148.
[abstract]
[postscript]
Also available as CSRG Technical Report 445.
-
with Andre Wong, "Formal Modeling in a Commercial Setting: A Case Study", Journal of Systems and Software, 60(1), pp. 57-80, January 2002. Also
available as CSRG Technical Report 392.
[abstract][postscript]
-
with Benet Devereux and Arie Gurfinkel, "XChek: A Multi-Valued Model-Checker",
in Proceedings of Computer-Aided Verification (CAV'02),
pp. 505-509, July 2002.
[postscript]
Also available as CSRG Technical Report 447.
-
with Wei Ding, "Lightweight Reasoning About Program Correctness".
Information Systems Frontiers, vol. 4, no. 4, November 2002,
pp. 363-377. (extended version of CASCON'01 paper).
[abstract]
[postscript].
2001
-
with Wei Ding, "Lightweight Reasoning About Program Correctness",
in Proceedings of CASCON'01, November 2001.
Also available as CSRG Technical Report 396.
[abstract]
[postscript]
-
"On Interpreting Results of Model-Checking with Abstraction",
submitted for publication, September 2001, 33 pages. [abstract] [postscript]. Also available
as CSRG Technical Report 417.
-
with Benet Devereux, Albert Lai, Steve Easterbrook and Victor
Petrovykh, "Efficient Multiple-Valued Model-Checking Using Lattice
Representations", in Proceedings of CONCUR'01,
August 2001.
[abstract]
[postscript]
[extended version].
Also available as CSRG Technical Report 429.
-
with Steve Easterbrook, "Automated Paraconsistent Reasoning via
Model Checking", in Proceedings of IJCAI Inconsistency Workshop,
August 2001, 8 pages.
[abstract] [postscript] Also available as CSRG Technical Report 428.
-
with J. Gannon, "Automatic Analysis of Consistency Between Requirements
and Designs", IEEE Transactions in Software Engineering, volume 27, number 7, July 2001.
[abstract]
[PDF]
Also available as CSRG technical Report 388.
-
with Steve Easterbrook, "Reasoning About Compositions of Concerns",
position paper in Proceedings of ICSE Workshop on
Advanced Separation of Concerns, May 2001, 5 pages.
[abstract] [postscript]
Also available as CRSG Technical Report 427.
-
with Steve Easterbrook, "A Framework to Handle Horizontal Inconsistency in Software", position paper in Proceedings of ICSE Workshop of
Living with Inconsistency, May 2001, 3 pages. [abstract]
[postscript].
-
with Kenneth Cheung, Yilan Gu, Arie Gurfinkel, Jiang Liu, Wendy Liu,
Wei Tjioe, Hung Tran, Clement Yuen,
"Automated Verification, Fall 2000: A Collection of Reports",
March 2001, available as a CSRG Technical Report 425.
[summary]
-
with Benet Devereux and Arie Gurfinkel, "Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN",
in Proceedings of SPIN Workshop on Model-Checking Software,
May 2001, 18 pages.
[abstract]
[postscript].
Also available as CRSG Technical Report 426.
-
with Steve Easterbrook and Benet Devereux,
"Model Checking with Multi-Valued Temporal Logics",
in Proceedings of International Symposium on
Multi-Valued Logics (ISMVL'01), May 2001, 6 pages.
[abstract]
[PDF].
Also available as CSRG Technical Report 430.
-
with Benet Devereux and Steve Easterbrook,
"Implementing a Multi-Valued Symbolic Model Checker",
in Proceedings of TACAS'01,
April 2001, 17 pages.
[abstract] [postscript]. Also available as CSRG Technical Report 431.
-
with Steve Easterbrook,
"A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints",
in Proceedings of International Conference on
Software Engineering (ICSE'01), May 2001, 11 pages.
[abstract] [postscript]. Also available as CSRG Technical Report 419.
-
with Steve Easterbrook and Victor Petrovykh,
"Model-Checking over Multi-Valued Logics", in Proceedings of
Formal Methods Europe (FME'01), March 2001. 26 pages.
[abstract] [postscript]. Also available as CSRG Technical Report 420.
2000
-
with William Andrepoulos,
Bob Bernecky,
Ariel Fuxman, Benet Devereux, Kristin Hofstee, Jingjing Lu, Tsuyoshi Morioka,
Peeter Piegaze, Jeffrey Tang, Sean Thompson, Cosmin Truta, Yuxiang Zhu, Wei Zhou, "Automated Verification, Fall 1999: A Collection of Reports",
March 2000, available as CSRG Technical Report 407.
[summary]
-
with Hai Wang, "Feasibility of Bisimulation Analysis of Protocols Expressed
in SDL", in Proceedings of CASCON'2000, pages 65-77,
November 2000.
Also available as CSRG Technical Report 382.
[abstract] [postscript]
1999
-
"SC(R)3: Towards Usability of Formal Methods" (extended version of the
paper published under the same name in Proceedings of CASCON'98), submitted
to Formal Methods in Software Design, August 1999, 37 pages. [abstract] [postscript] Also available
as CSRG Technical Report 391.
-
with Ma Chuan, Veronika Cwir, Ken Pu, Su Rong, Yuwei Wang, "Automated Verification, Spring 1999: A Collection of Reports", June 1999, available as
CSRG Technical Report 380. [summary]
-
with Dimi Paun, "Events in Property Patterns", in
Theoretical and Practical Aspects of SPIN Model Checking,
LNCS 1680, pp. 154-167,
September 1999.
[abstract] [postscript]. Also available as CSRG Technical Report 381.
-
with Andre Wong, "Formal Methods When Money Is Tight",
position paper, in Proceedings of the 1st Workshop on Economics-Driven
Software Engineering Research (EDSER-1), May 1999. [postscript] Also available
as CSRG Technical Report 383.
- with Andre Wong, "Formal Modeling in a Commercial Setting: A Case
Study", Proceedings of World Congress in Formal
Methods (FM'99), September 1999. [abstract]
[postscript]
Also available as CSRG Technical Report 385.
-
with Dimi Paun, "Events in Linear-Time Properties", in
Proceedings of Requirements Engineering, June 1999. [abstract]
[postscript]
Also available as CSRG Technical Report 384.
1998
-
"Using SCR Requirements", position paper, in Proceedings of the 7th
SCR workshop, October 1998. [postscript]
-
with Andre Wong, "Applying Formal Methods to a Telecommunications
System in a Commercial Setting", position paper, in Proceedings of
11th International Conference on Software Engineering and Its
Applications, December 1998. [abstract]
[postscript]
Also available as CSRG Technical Report 377.
-
"SC(R)3 - Towards Usability of Formal Methods", in
Proceedings of CASCON, November 1998. [abstract]
[postscript]
Also available as CSRG Technical Report 386.
-
with Dimi Paun and Bernd Biechele, "Production Cell Revisited", in
Proceedings of SPIN'98, November 1998.
[abstract]
[postscript]
Also available as CSRG Technical Report 387.
-
with students of csc2108, Fall'97, "Automated Verification: A Collection
of Reports", CSRG Technical Report 374, Department of Computer Science,
University of Toronto, April, 1998. [summary]
1997
-
with S. Vallurupalli, "Checking Consistency Between Source Code and Annotations",
CSRG technical report 373, University of Toronto, December 1997.
[abstract]
-
Software Engineering Education at the University of Toronto, a position
paper in Proceedings
of the 4th Software Engineering Workshop, May 1997.
1996
-
Automatic Analysis of Consistency between Requirements and Designs, Ph.D.
Thesis, University of Maryland, College Park, December 1996.
[abstract]
[postscript]
-
with J. Gannon, "Verification of Consistency Between Concurrent
Program Designs and Their Requirements", in Proceedings of
Symposium on Computer Assurance (COMPASS'96), Gathersburg, MD,
June 1996. [abstract]
[postscript]
-
with J. Atlee and J. Gannon, "Using Model Checking to Analyze
Requirements and Designs", in Advances in Computers, Volume 43, Marv
Zelkowitz, ed. Academic Press, 1996. [abstract]
[postscript]
1995
-
with J. Gannon, "Automatic Analysis of Consistency Between
Implementations and Requirements: A Case Study", in Proceedings of
Symposium on Computer Assurance (COMPASS'95), pp. 123-132,
Gathersburg, MD, June 1995. [abstract]
[postscript]
1994
-
with J. Gannon, "Automatic Verification of Requirements
Implementation", in Proceedings of International Symposium on
Testing and Analysis (ISSTA'94), pp. 1-15, Seattle, August 1994.
[abstract]
[postscript]
Marsha Chechik