Z Specification of an Object Manager. - Patrice Chalin; Peter Grogono (VDM Europe, 1990)

Copying, Sharing, and Aliasing. - Peter Grogono; Patrice Chalin (COODBSE, 1994)

Identification of and Solutions to Shortcomings of LCL, a Larch/C Interface Specification Language. - Patrice Chalin; Peter Grogono; Thiruvengadam Radhakrishnan (FME, 1996)

Improving JML: For a Safer and More Effective Language. - Patrice Chalin (FME, 2003)

JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics. - Patrice Chalin (J. Object Technol., 2004)

Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. - Patrice Chalin; Joseph R. Kiniry; Gary T. Leavens; Erik Poll (FMCO, 2005)

Logical Foundations of Program Assertions: What do Practitioners Want?. - Patrice Chalin (SEFM, 2005)

Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. - Joseph R. Kiniry; Patrice Chalin; Clément Hurlin (VSTTE, 2005)

Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study. - Frédéric Rioux; Patrice Chalin (WWV, 2005)

Are Practitioners Writing Contracts? - Patrice Chalin (RODIN Book, 2006)

Early detection of JML specification errors using ESC/Java2. - Patrice Chalin (SAVCBS@FSE, 2006)

The KOA Remote Voting System: A Summary of Work to Date. - Joseph R. Kiniry; Alan E. Morkan; Dermot Cochran; Fintan Fairmichael; Patrice Chalin; Martijn Oostdijk; Engelbert Hubbers (TGC, 2006)

Towards a Common Semantic Foundation for Use Cases and Task Models. - Daniel Sinnig; Patrice Chalin; Ferhat Khendek (FMIS@ICFEM, 2006)

Non-null references by default in the Java modeling language. - Patrice Chalin; Frédéric Rioux (ACM SIGSOFT Softw. Eng. Notes, 2006)

Non-null References by Default in Java: Alleviating the Nullity Annotation Burden. - Patrice Chalin; Perry R. James (ECOOP, 2007)

Consistency between Task Models and Use Cases. - Daniel Sinnig; Patrice Chalin; Ferhat Khendek (EHCI/DS-VIS, 2007)

A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler. - Patrice Chalin (ICSE, 2007)

Common Semantics for Use Cases and Task Models. - Daniel Sinnig; Patrice Chalin; Ferhat Khendek (IFM, 2007)

An integrated verification environment for JML: architecture and early results. - Patrice Chalin; Perry R. James; George Karabotsos (SAVCBS, 2007)

Practical Extensions for Task Models. - Daniel Sinnig; Maik Wurdel; Peter Forbrig; Patrice Chalin; Ferhat Khendek (TAMODIA, 2007)

Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations? - Patrice Chalin (Formal Aspects Comput., 2007)

JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity. - Patrice Chalin; Frédéric Rioux (FM, 2008)

Capturing business transaction requirements in use case models. - Patrice Chalin; Daniel Sinnig; Kianoush Torkzadeh (SAC, 2008)

JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. - Patrice Chalin; Perry R. James; George Karabotsos (VSTTE, 2008)

Reducing the use of nullable types through non-null by default and monotonic non-null. - Patrice Chalin; Perry R. James; Frédéric Rioux (IET Softw., 2008)

Preliminary design of a unified JML representation and software infrastructure. - Robby; Patrice Chalin (FTfJP@ECOOP, 2009)

Extended static checking in JML4: benefits of multiple-prover support. - Perry R. James; Patrice Chalin (SAC, 2009)

LTS semantics for use case models. - Daniel Sinnig; Patrice Chalin; Ferhat Khendek (SAC, 2009)

Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less. - Patrice Chalin (SEFM, 2009)

ESC4: a modern caching ESC for Java. - Perry R. James; Patrice Chalin (SAVCBS, 2009)

Merging of Use Case Models: Semantic Foundations. - Stephen C. Barrett; Daniel Sinnig; Patrice Chalin; Greg Butler (TASE, 2009)

Mirador: a synthesis of model matching strategies. - Stephen C. Barrett; Greg Butler; Patrice Chalin (IWMCP@ICMT, 2010)

A Formal Model for Generating Integrated Functional and User Interface Test Cases. - Daniel Sinnig; Ferhat Khendek; Patrice Chalin (ICST, 2010)

Faster and More Complete Extended Static Checking for the Java Modeling Language. - Perry R. James; Patrice Chalin (J. Autom. Reason., 2010)

Towards an industrial grade IVE for Java and next generation research platform for JML. - Patrice Chalin; Robby; Perry R. James; Jooyong Lee; George Karabotsos (Int. J. Softw. Tools Technol. Transf., 2010)

Engineering a Sound Assertion Semantics for the Verifying Compiler. - Patrice Chalin (IEEE Trans. Software Eng., 2010)

Table-Driven Detection and Resolution of Operation-Based Merge Conflicts with Mirador. - Stephen C. Barrett; Patrice Chalin; Greg Butler (ECMFA, 2011)

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (NASA Formal Methods, 2011)

Enhancing spark's contract checking facilities using symbolic execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (SIGAda, 2011)

Partial order semantics for use case and task models. - Daniel Sinnig; Ferhat Khendek; Patrice Chalin (Formal Aspects Comput., 2011)

Requirements specification for apps in medical application platforms. - Brian R. Larson; John Hatcliff; Sam Procter; Patrice Chalin (SEHC@ICSE, 2012)

Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. - Jason Belt; Robby; Patrice Chalin; John Hatcliff; Xianghua Deng (NASA Formal Methods, 2012)

Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. - Jason Belt; Patrice Chalin; John Hatcliff; Robby (HILT, 2012)

A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar. - Loren Segal; Patrice Chalin (VSTTE, 2012)

Explicating symbolic execution (xSymExe): an evidence-based verification framework. - John Hatcliff; Robby; Patrice Chalin; Jason Belt (ICSE, 2013)

Open source patient-controlled analgesic pump requirements documentation. - Brian R. Larson; John Hatcliff; Patrice Chalin (SEHC@ICSE, 2013)

BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software. - Brian R. Larson; Patrice Chalin; John Hatcliff (NASA Formal Methods, 2013)

Use case and task models: An integrated development methodology and its formal foundation. - Daniel Sinnig; Patrice Chalin; Ferhat Khendek (ACM Trans. Softw. Eng. Methodol., 2013)

Ensuring that your dart will hit the mark: An introduction to dart contracts. - Patrice Chalin (IRI, 2014)