Papers archive | Programming Languages & Verification

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
J. Funct. Program. 2007.

Game Relations and Metrics.

Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga.
LICS 2007.

Tasks: language support for event-driven programming.

Jeffrey Fischer, Rupak Majumdar, Todd D. Millstein.
PEPM 2007.

Path invariants.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko.
PLDI 2007.

Interprocedural analysis of asynchronous programs.

Ranjit Jhala, Rupak Majumdar.
POPL 2007.

Lock allocation.

Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar.
POPL 2007.

Modular Safety Checking for Fine-Grained Concurrency.

Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis.
SAS 2007.

The software model checker Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
STTT 2007.

State of the Union: Type Inference Via Craig Interpolation.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu.
TACAS 2007.

Invariant Synthesis for Combined Theories.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko.
VMCAI 2007.

Verifying Compensating Transactions.

Michael Emmi, Rupak Majumdar.
VMCAI 2007.

Decision Problems for the Verification of Real-Time Software.

Michael Emmi, Rupak Majumdar.
HSCC 2006.

Sudoku as a SAT Problem.

Inês Lynce, Joël Ouaknine.
ISAIM 2006.

Proving correctness of highly-concurrent linearisable objects.

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
PPOPP 2006.

Compositional Quantitative Reasoning.

Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga.
QEST 2006.

Structural Invariants.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu.
SAS 2006.

Bit level types for high level reasoning.

Ranjit Jhala, Rupak Majumdar.
SIGSOFT FSE 2006.

Interpolation for data structures.

Deepak Kapur, Rupak Majumdar, Calogero G. Zarba.
SIGSOFT FSE 2006.

Markov Decision Processes with Multiple Objectives.

Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger.
STACS 2006.

On the universal and existential fragments of the mu -calculus.

Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar.
Theor. Comput. Sci. 2006.

A classification of symbolic transition systems.

Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin.
ACM Trans. Comput. Log. 2005.

Verifying Quantitative Properties Using Bound Functions.

Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar.
CHARME 2005.

Code aware resource management.

Luca de Alfaro, Vishwanath Raman, Marco Faella, Rupak Majumdar.
EMSOFT 2005.

Joining dataflow with predicates.

Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar.
ESEC/SIGSOFT FSE 2005.

Permissive interfaces.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
ESEC/SIGSOFT FSE 2005.

Checking Memory Safety with Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
FASE 2005.

Quantifying Similarities Between Timed Systems.

Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu.
FORMATS 2005.

Acute: high-level programming language design for distributed computation.

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
ICFP 2005.

Path slicing.

Ranjit Jhala, Rupak Majumdar.
PLDI 2005.

Verification of Reactive Systems: Formal Methods and Algorithms. By Klaus Schneider. Springer, Texts in Theoretical Computer Science Series, 2004, ISBN: 3-540-00296-0, pp 600.

Joël Ouaknine.
Softw. Test., Verif. Reliab. 2005.