Pavol Cerny's homepage

Pavol Cerny

Name (TeX style): Pavol \v{C}ern\'y
Ph.D. student

Advisor: prof. Rajeev Alur
Department of Computer and Information Science
University of Pennsylvania

e-mail: cernyp at cis upenn edu

Contact

CV [pdf]

Personal page

News

I have moved to IST Austria, where I have joined Tom Henzinger's group as a postdoc.

Research interests

Software model checking and program analysis. Algorithms, models and logics for computer-aided verification. Specifically, I have worked on verification of concurrent programs, software model checking for confidentiality, electronic voting security, programming abstractions for data parallel programs, synthesis of interface specifications for Java classes and abstract interpretation with parameterized predicates.

Teaching

CSE 399: C/C++ programming. Co-instructor, Spring 2006.
CIS 399-002: C++ programming. Instructor, Spring 2009.

Teaching Assistantship

CSE 482: Logic in Computer Science. Fall 2004.
CIS 511: Theory of Computation. Spring 2005.

Publications

Peer reviewed

Algorithmic Analysis of Array-Accessing Programs.
    Rajeev Alur, Pavol Cerny and Scott Weinstein
    18th Conference on Computer Science Logic
    CSL 2009, Coimbra, Portugal, September 7-11, 2009
    [pdf] [bibtex]
Parallel Programming with Object Assemblies.
    Swarat Chaudhuri, Roberto Lublinerman, and Pavol Cerny.
    24th Conference on Object-Oriented Programming, Systems, Languages, and Applications
    OOPSLA 2009, Orlando, FL, USA, October 25-October 29, 2009
    [pdf]
Automated Analysis of Java Methods for Confidentiality.
    Pavol Cerny and Rajeev Alur.
    21st International Conference on Computer Aided Verification
    CAV 2009, Grenoble, France, June 28-July 2, 2009
    [pdf] [bibtex]
Assemblies of Objects.
    Swarat Chaudhuri, Roberto Lublinerman, and Pavol Cerny.
    2nd Workshop on Exploiting Concurrency Efficiently and Correctly
    EC2 2009, Grenoble, France, June 26-27, 2009
    [pdf]
Security Evaluation of ES&S Voting Machines and Election Management System.
    Adam Aviv, Pavol Cerny, Sandy Clark, Eric Cronin, Gaurav Shah, Micah Sherr, and Matt Blaze.
    3rd USENIX/ACCURATE Electronic Voting Technology workshop
    EVT 2008, San Jose, California, USA, July 28-29, 2008.
    [pdf] [bibtex]
Model Checking on Trees with Path Equivalences
    Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri.
    13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
    TACAS 2007, Braga, Portugal, March 24-April 1, 2007
    "Best paper coauthored by a student" award.
    [pdf] [bibtex]
Preserving Secrecy under Refinement
    Rajeev Alur, Pavol Cerny, and Steve Zdancewic.
    33rd International Colloquium on Automata, Languages and Programming,
    ICALP 2006, Venice, Italy, Jul 9-14, 2006.
    [pdf] [bibtex]
Synthesis of Interface Specifications for Java Classes
    Rajeev Alur, Pavol Cerny, P. Madhusudan, and Wonhong Nam.
    32nd Annual ACM SIGPLAN-SIGACT Symp. on Principles of Prog. Languages,
    POPL 2005, Long Beach, California, USA, Jan 12-14, 2005.
    [pdf] [bibtex]

Theses, Reports, Posters

Software Model Checking for Confidentiality.
    Pavol Cerny
    PhD thesis, University of Pennsylvania, July 2009
    [pdf] [bibtex]
EVEREST: Evaluation and Validation of Election-Related Standards and Testing.
    A study of electronic voting systems for the state of Ohio. Available here on the website of the Ohio Secretary of State.
    December 2007
    See a statement by the project PIs, or a shorter write-up.
Analyzing Confidentiality for Programs.
Rajeev Alur, Pavol Cerny, Andre Scedrov and Steve Zdancewic.
Poster for NSF Cyber Trust PI Meeting, 2008.
Model Checking of Secrecy Properties.
Rajeev Alur, Pavol Cerny, Andre Scedrov and Steve Zdancewic.
Poster for NSF Cyber Trust PI Meeting, 2007.
Analysis of Concurrent Software.
Written Preliminary Examination report, 2005.
Verification by Abstract Interpretation of Parameterized Predicates.
DEA diploma thesis, 2003. Ecole normale superieure (ENS), Paris, France

Tool

JIST - Java Interface Synthesis Tool

(Older) Talks

Model Checking on Trees with Path Equivalences [ppt]
March, 2007 at TACAS 2007
Preserving Secrecy Under Refinement [ppt]
July 10, 2006 at ICALP 2006
Verification by Abstract Interpretation of Parameterized Predicates [pdf] [ps]
September 26, 2003 at SAI seminar, DI, ENS
Static Analyses for Efficient Execution of PVS [pdf] [ps]
July 12, 2002 at CSL, SRI International