• Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus2013-12-17
• When is a formula invariant?2013-11-26
• Towards model checking the hardware description language BSV2013-11-21
• Rule Formats for Structural Operational Semantics: A Very Short Introduction2013-11-18
• Symbolic-Numeric Algorithms for Verified Computations2013-11-14
• Modular Construction of Shape-Numeric Analyzers2013-11-11
• Small Bug, Big Bang2013-10-25
• The Parameterized Complexity of Counting k-Matchings2013-10-24
• 中国科学院“爱因斯坦讲席教授”、图灵奖获得者Edmund M. Clarke教授来访2013-10-22
• Automatic Generation of Program Invariants from Traces2013-10-11
• Three Lectures on Model Checking2013-10-09
• Automatic Testing-Based Formal Verification: Bridging Testing and Formal Verification for Program Correctness2013-09-09
• Mu and mu tilde: two useful combinators2013-08-29
• Mathematics and Physics Foundation for Digital Medicine in Virtual Environments2013-08-22
• On Two Challenging Problems in Statistical Debugging2013-08-21
• Advances in symbolic model checking for multi-agent systems2013-08-05
• Program debugging with effective software fault localization2013-07-17
• Uniform Monte Carlo Model Checking2013-07-17
• Model-Checking Iterated Games2013-07-10
• Equational Reasoning and Unification in Protocol Verification2013-07-09