Welcome to my public academic web page. Since August 2011, I am an Associate Professor in the Computing and Information Sciences Department (CIS) at Kansas State University (KSU) and, and member of the SAnToS Laboratory. 

I also have pages on LinkedIn and Google+ (and publication lists via DBLP and Google Scholar as pointed out below).

Research Areas and Projects

Teaching

Publications

The most complete list of my publications is available from Google Scholar, DBPL, ACM (author page; keyword search). Selected publications are included below:

• D. Sinnig, P. Chalin, F. Khendek, "Use case and task models: An integrated development methodology and its formal foundation". ACM Trans. Softw. Eng. Methodol. 22(3): 27 (2013).
•  B. Larson, J. Hatcliff, P. Chalin, “Open Source Patient-Controlled Analgesic Pump Requirements Documentation”. Proc. of the Fifth International Workshop on Software Engineering in Health Care (SEHC), San Francisco, May 2013.
• B.R. Larson, P. Chalin, J. Hatcliff. "BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software".  NASA Formal Methods Symposium (NFM) 2013.
• J. Hatcliff, Robby, P. Chalin, J. Belt. “Explicating Symbolic Execution (xSymExe): An Evidence-based Verification Framework”. Proc. of the International Conference on Software Engineering (ICSE), 2013. [18.5%]
• J. Belt, Robby, P. Chalin, J. Hatcliff and X. Deng. Efficient Symbolic Execution of Programs for Critical Systems. Proc. of the NASA Formal Methods Conference (NFM), 2012 [39%].
• L. Segal and P. Chalin, “A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar”. Proceedings of the International Conference on Verified Software: Theories, Tools, Exper-iments (VSTTE), Philadelphia, USA, January, pp. 130-145, 2012 [37%].
• D. Sinnig, F. Khendek, and P. Chalin, “Partial Order Semantics for Use Case and Task Models”, Formal Aspects of Computing, 23(3):307-332, 2011.
• P. Chalin, “Engineering a Sound Assertion Semantics for the Verifying Compiler”, IEEE Transactions on Software Engineering, 36(2):275-287, 2010. DOI; appendix.
• P. R. James and P. Chalin, “Faster and More Complete Extended Static Checking for the Java Modeling Language”, J. Automated Reasoning, 44(1-2):145-174, 2010. (SpringerLink)
• S. Barrett, P. Chalin, and G. Butler, “Table-Driven Detection and Resolution of Operation-Based Merge Conflicts in Mirador”. Proceedings of the European Conference on Modelling Foundations and Applications (ECMFA), Birmingham, UK, 2011.
• S. Barrett, G. Butler, and P. Chalin, “Mirador: a Synthesis of Model Matching Strategies”. Proceedings of the International Workshop on Model Comparison in Practice (IWMCP), Malaga, Spain, July, 2010.
• P. Chalin, “Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less”. Proceedings of the Software Engineering and Formal Methods (SEFM), Hanoi, Vietnam, Nov. 2009 (slides). [26.7% (35.7%)]
• P. Chalin, P. R. James, and F. Rioux, “Reducing the Use of Nullable Types through Non-null by Default and Monotonic Non-null”, IET Software Journal, 2(6):515-531, 2008. DOI.
• P. Chalin, “Are the Logical Foundations of Verifying Compiler Prototypes Matching User Expectations?” Formal Aspects of Computing , 19(2):139-158, 2007.
• P. Chalin, “Are Practitioners Writing Contracts?” in Rigorous Development of Complex Fault-Tolerant Systems, LNCS 4157, M. Butler, C. B. Jones, A. Romanovsky, and E. Troubitsyna, Eds.: Springer, pp. 100-113, 2006. DOI.

Other links