Pavol Cerny's homepage

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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

Links

Research interests

Algorithms, models and logics for computer-aided verification . Specifically, my research is on algorithmic verification of software for secrecy and other information flow properties. I have also worked on synthesis of interface specifications for Java classes, abstract interpretation with parameterized predicates, and electronic voting security.

Teaching

CSE 399: C/C++ programming. Co-instructor, Spring 2006.

Teaching Assistantship

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

Publications

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.
    To appear.
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]

Reports, Posters

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

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