2024.01.19

CUPLV authors Benno Stein and Bor-Yuh Evan Chang with collaborators has had a paper "Interactive Abstract Interpretation with Demanded Summarization" published in TOPLAS.

2023.11.01

Call for Ph.D. applicants for Fall 2024. Application deadline is December 15, 2023.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL, PLDI, and CAV. CS Admissions and ECEE Admissions (deadline December 15, 2023).

2023.07.01

CUPLV authors Shawn Meier, Kirby Linvill, Sergio Mover, Gowtham Kaki, and Bor-Yuh Evan Chang have had papers accepted for presentation at OOPSLA 2023 in October (Meier et al. and Linvill et al.).

2023.06.29

CUPLV author Bor-Yuh Evan Chang with collaborators has had a paper "Lifting On-Demand Analysis to Higher-Order Languages" accepted for presentation at SAS 2023 in October.

2022.11.01

Call for Ph.D. applicants for Fall 2023. Application deadline is December 15, 2022.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL, PLDI, and CAV. CS Admissions and ECEE Admissions (deadline December 15, 2022).

2022.02.25

CUPLV authors Gowtham Kaki, Prasanth Prahladan, and Nicholas V. Lewchenko have had papers accepted for presentation at PLDI 2022 in June (Kaki et al. and Žikelić et al.).

2021.11.01

Call for Ph.D. applicants for Fall 2022. Application deadline is December 15, 2021.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL, PLDI, and CAV. CS Admissions and ECEE Admissions (deadline December 15, 2021).

2021.10.13

Tianhan Lu wins the Radhia Cousot Young Researcher Best Paper Award at SAS 2021 for his paper "Selectively-Amortized Resource Bounding" co-authored with Bor-Yuh Evan Chang and Ashutosh Trivedi.

2021.09.29

CUPLV student Benno Stein receives the 2021 Ralph J. Slutz Student Excellence Award.

2021.07.05

CUPLV authors Tianhan Lu, Bor-Yuh Evan Chang, and Ashutosh Trivedi, have had a paper "Selectively-Amortized Resource Bounding" accepted for presentation at SAS 2021 in October.

2021.04.19

CUPLV student Benno Stein receives the 2020-2021 CU CS Outstanding Research Award.

2021.04.18

CUPLV authors Mateo Perez, Fabio Somenzi, and Ashutosh Trivedi with collaborators, have had a paper "Model-Free Reinforcement Learning for Branching Markov Decision Processes." accepted for presentation at CAV 2021 in July.

2021.02.25

CUPLV authors Benno Stein and Bor-Yuh Evan Chang with collaborators have had a paper "Demanded Abstract Interpretation" accepted for presentation at PLDI 2021 in June.

2020.11.12

CUPLV author Bor-Yuh Evan Chang with collaborators have had a survery paper "Shape Analysis" published in FNTPL.

2020.11.01

Call for Ph.D. applicants for Fall 2021. Application deadline is December 15, 2020.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL, PLDI, and CAV. CS Admissions and ECEE Admissions (deadline December 15, 2020).

2020.04.05

CUPLV authors Sriram Sankaranarayanan and Majid Zamani with collaborators have had papers accepted for presentation at CAV 2020 in July (Sankaranarayanan et al., Feng et al., Devonport et al., and Lavaei et al.).

2019.11.01

Please consider applying or encourage your students and postdocs to apply for positions in the Department of Computer Science. We have multiple openings with one particular interest area being trustworthy software. Applications will be evaluated beginning on December 1, 2019, although applications will continue to be evaluated until the position is filled.

Tenure-Track and Instructor Positions


          The majestic, snow-covered Flatirons is a breathtaking backdrop with Old Main at the University of Colorado Boulder in the foreground. (Photo by Casey A. Cass/University of Colorado)
Apply for a Tenure-Track Position in Trustworthy Software. The Department of Computer Science at the University of Colorado Boulder is currently seeking applications for a tenure-track faculty position in the area of secure and reliable software. This includes, but is not limited to, a broad swath of topics, including programming language foundations (e.g., type systems, language design), large-scale distributed systems (e.g., cloud computing), secure software (e.g., language-based security), probabilistic programming (e.g., languages for machine learning), automated reasoning (e.g., program analysis, software verification), industrial-scale computing (e.g., software engineering), and computing education research. However, many promising candidates may not identify their work under any of the specific areas listed. Such candidates are encouraged to contact the search chair (see below).

The position is open at all levels, with emphasis on applicants at the Assistant Professor level. Candidates whose expertise cuts across engineering and related disciplines are especially encouraged to apply.

We are especially interested in qualified candidates who can contribute, through their research, teaching, and service, to the diversity and excellence of our academic community. Our university is also responsive to dual career situations.

This position is part of the long-term growth plans for the College of Engineering and Applied Science (CEAS). CEAS is the highest ranked engineering college in the Rocky Mountain time zone and hosts several nationally ranked departments. The Department of Computer Science has 2500 undergraduate students, 369 graduate students and 69 faculty. The Department's research and education efforts interact broadly with many interdisciplinary programs and collaborators in the Boulder area, including national labs at NIST, NOAA, NREL, and NCAR, and CU Boulder research institutes including the ATLAS Institute, the BioFrontiers Institute, and the Institute for Cognitive Science. More than 20 faculty members have joint affiliations with one of these labs. The Department also has a long-standing partnership with the National Center for Women and IT and has faculty active in increasing the broadening of participation in computer science via their research, teaching, and service. In addition, the Department has extensive ties with the thriving local tech community and inhabits a picturesque location in the foothills of the Rocky Mountains.

Candidates will be expected to engage in undergraduate and graduate teaching, contribute professional service, and develop vigorous, externally funded research programs in their technical areas. Potential faculty members applying to the Department of Computer Science at the University of Colorado Boulder should describe their plans to develop a recognized research program based on scholarly work in their particular field, their ideas for interdisciplinary collaboration, their experience and interests in teaching undergraduates and graduates, and their future plans for inspiring diverse students to conduct research.

The position will remain open until filled, though for full consideration applications should be received by December 1, 2019.

Apply for an Instructor Position. The Department of Computer Science in the College of Engineering and Applied Science at the University of Colorado Boulder invites applications for a full-time Instructor position. This position will support the Department of Computer Science and fulfillment of the department’s educational mission through teaching Computer Science courses on the CU-Boulder campus.

Candidates must demonstrate a strong commitment to high-quality undergraduate education. We are particularly interested in candidates with a background in the areas of algorithms, databases, software engineering, or programming languages.

Applications will be accepted until the position is filled.

2019.11.01

Call for Ph.D. applicants for Fall 2020. Application deadline is December 15, 2019.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL, PLDI, and CAV. CS Admissions and ECEE Admissions (deadline December 15, 2019).

2019.08.30

CUPLV authors Benno Stein and Bor-Yuh Evan Chang with collaborators have had a paper "Static Analysis with Demand-Driven Value Refinement" accepted for presentation at OOPSLA 2019 in October.

2019.07.01

CUPLV authors Saeid Tizpaz Niari, Hansol Yoon, Chou Yi, Pavol Černý, Sriram Sankaranarayanan, and Ashutosh Trivedi with collaborators have had papers accepted for presentation at RV 2019 in October (Niari et al., Yoon et al., and Fainekos et al.).

2019.06.24

CUPLV researchers Sergio Mover and Sriram Sankaranarayanan represents the Fixr Team at GitHub in San Francisco.

Fixr Team at GitHub


          Fixr Team at GitHub.

2019.06.14

CUPLV authors Nicholas V. Lewchenko, Akash Gaonkar, and Pavol Černý with collaborators have had a paper "Sequential Programming for Replicated Data Stores" accepted for presentation at ICFP 2019 in August.

2019.04.17

CUPLV authors Saeid Tizpaz Niari, Pavol Černý, and Ashutosh Trivedi have had a paper "Quantitative Mitigation of Timing Side Channels" accepted for presentation at CAV 2019 in July.

2019.03.31

CUPLV authors Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang have had a paper "Lifestate: Event-Driven Protocols and Callback Control Flow" accepted for presentation at ECOOP 2019 in July.

2018.11.23

CUPLV authors Tianhan Lu Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi have had a paper "Type-directed Bounding of Collections in Reactive Programs" accepted for presentation at VMCAI 2019 in January.

2018.10.23

CUPLV student Taisa Kushner receives the 2018 Ralph J. Slutz Student Excellence Award.

2018.08.01

CUPLV student Shawn Meier pitched at Catalyze CU Demo Day 2018.

2018.07.03

CUPLV authors Benno Stein and Bor-Yuh Evan Chang with collaborators have had a paper "Safe Stream-Based Programming with Refinement Types" accepted for presentation at ASE 2018 in September.

2018.06.19

CUPLV authors Souradeep Dutta Taisa Kushner, and Sriram Sankaranarayanan have had a paper "Robust Data-Driven Control of Artificial Pancreas Systems using Neural Networks" accepted for presentation at CMSB 2018 in September.

2018.06.01

CUPLV Postdoctoral Scholar Sergio Mover accepts a position as a Gaspard Monge Assistant Professor in Computer Science at École Polytechnique.

2018.05.07

CUPLV PhD Student Jedidiah McClurg accepts a position as an assistant professor of comptuer science at the University of New Mexico.

2018.04.06

CUPLV PhD Student Saeid Tizpaz Niari wins the 2018 Gold Research Award from ECEE.

ECEE Research Award


          Saeid Tizpaz Niari with his award!
Congratulations, Saeid!

2018.03.23

CUPLV authors Sergio Mover, Sriram Sankaranarayanan, Rhys Braginton Pettee Olsen, and Bor-Yuh Evan Chang win the IEEE TCSE Distinguished Paper Award at SANER 2018 for "Mining Framework Usage Graphs from App Corpora."

2018.03.22

CUPLV researchers Shawn Meier and Bor-Yuh Evan Chang with collaborators came in 3rd in the R&D track of New Venture Challenge 10, earning $1,000 for the venture.

NVC10


          Lambda Leaf with their award!
Congratulations, Shawn!

2018.02.14

Prospective Ph.D. students visit February 16. Welcome!

2017.12.20

CUPLV authors Fabio Somenzi and Ashutosh Trivedi with collaborators have had a paper "Almost-Sure Reachability in Stochastic Multi-Mode System" accepted for presentation at HSCC 2018 in April.

2017.12.19

CUPLV authors Taisa Kushner and Sriram Sankaranarayanan with collaborators have had a paper "A Data-Driven Approach to Artificial Pancreas Verification and Synthesis" accepted for presentation at ICCPS 2018 in April.

2017.12.17

CUPLV authors Sergio Mover, Sriram Sankaranarayanan, Rhys Braginton Pettee Olsen, and Bor-Yuh Evan Chang have had a paper "Mining Framework Usage Graphs from App Corpora" accepted for presentation at SANER 2018 in March.

2017.12.13

CUPLV authors Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Bor-Yuh Evan Chang, and Pavol Černý with collaborators have had a paper "DroidStar: Callback Typestates for Android Classes" accepted for presentation at ICSE 2018 in May.

2017.12.11

CUPLV authors Xin Chen, Sergio Mover, and Sriram Sankaranarayanan nominated for an ACM SIGBED EMSOFT Best Paper Award for "Compositional Relational Abstraction for Nonlinear Hybrid Systems."

2017.11.28

CUPLV authors Saeid Tizpaz Niari, Pavol Černý, Bor-Yuh Evan Chang, and Ashutosh Trivedi have had a paper "Differential Performance Debugging with Discriminant Regression Trees" accepted for presentation at AAAI 2018 in February.

2017.08.02

CUPLV authors Edmund S.L. Lam, Peilun Zhang, and Bor-Yuh Evan Chang have had a paper "ChimpCheck: Property-Based Randomized Test Generation for Interactive Apps" officially accepted for presentation at ONWARD! 2017 in October.

2017.06.30

CUPLV authors Xin Chen, Sergio Mover, and Sriram Sankaranarayanan have had a paper "Compositional Relational Abstraction for Nonlinear Hybrid Systems" accepted for presentation at EMSOFT 2017 in October.

2017.06.22

Bor-Yuh Evan Chang promoted to Associate Professor and granted tenure.

2017.06.21

Congratulations to Kyle Headley for being awarded second place in the graduate student category at the PLDI Student Research Competition (SRC) for his project, "Tuning Data and Control Structures for Incremental Computation."

2017.06.21

Congratulations to Peilun Zhang for being awarded first place in the undergraduate student category at the PLDI Student Research Competition (SRC) for his project, "Property-based Randomized Test Generation for Android Applications."

2017.05.23

There is a postdoctoral research associate position open with the opportunity to work with Profs. Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi on program analysis.

Postdoc Position


      The majestic, snow-covered Flatirons is a breathtaking backdrop with Old Main at the University of Colorado Boulder in the foreground. (Photo by Casey A. Cass/University of Colorado)
The Programming Languages and Verification Group at the University of Colorado Boulder (CUPLV) is looking for exceptional candidates for a postdoctoral research associate in the area of program analysis.

The ideal candidate has a background in the area of programming languages and verification, as well as an enthusiasm for mentoring junior researchers.

The postdoctoral researcher would collaborate with Profs. Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi. The researcher will have an opportunity to lead an ambitious project on program analysis for security. To apply, please send an email to Pavol Černý with a CV and contact information for two or three references.

Our group has active projects in areas such as the following:

The position is for one year, with a possible extension for additional years. Highly-qualified candidates may be considered for a research assistant professor position. Teaching opportunities will be available. Compensation is highly competitive and commensurate with experience.

Boulder, located at the base of the Rocky Mountains, is consistently awarded top-rankings for health, education, and quality of life. It is also home to a concentration of high-tech industry and to a vibrant startup community. It is located 30 miles from downtown Denver.

2017.04.28

CUPLV authors Hadi Ravanbakhsh and Sriram Sankaranarayanan have had a paper "Learning Lyapunov (Potential) Functions from Counterexamples and Demonstrations" accepted for presentation at RSS 2017 in October.

2016.12.22

CUPLV authors Saeid Tizpaz Niari Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi have had a paper "Discriminating Traces with Time" accepted for presentation at TACAS 2017 in April.

2016.10.26

Bo Wu from Colorado School of Mines is visiting us on October 28, 2016. He is giving a CUPLV Seminar entitled "Compiler and Runtime Optimizations for GPU Memory Systems" at 3:00pm in KOBL 230 on Friday, October 28, 2016.

PLV Seminar

Bo Wu
Colorado School of Mines

10-28-2015 15:00
KOBL 230

Compiler and Runtime Optimizations for GPU Memory Systems

Abstract

In recent year, we have seen a rapid rise of massive parallelism in modern processors, exemplified by GPUs, APUs and MIC processors. The emergence of massive parallelism in a single node brings growing demands for efficient data accesses. Optimizing memory throughput is hence critical for tapping into the full potential of the many-core systems. In the first half of the talk, I will present some theoretical and empirical results on optimizing memory coalescing for GPUs. In the second half of the talk, I will present our framework to automatically place data on GPUs for performance and portability.

Biography

Bo Wu is an Assistant Professor in the EECS department at Colorado School of Mines. He received his Ph.D. degree in computer science from the College of William and Mary for his dissertation on "Matching Non-Uniformity for Program Optimizations on Heterogeneous Manycore Systems”. He received his M.S. degree in computer science and B.S. degree in mathematics both from Central South University in China. His research interests lie in the broad field of compilers and programming systems, with an emphasis on program optimizations for heterogeneous computing and emerging architectures. Most of his research activities have centered around data locality enhancement for heterogeneous computing systems.

Hosted by Bor-Yuh Evan Chang.

2016.10.26

Georgios Fainekos from Arizona State University is visiting us on October 27, 2016. He is giving a Computer Science Colloquium entitled "Beyond Requirements Falsification : Semi-Formal Methods and Tools for the Analysis of Cyber-Physical Systems" at 3:30pm in ECCR 265 on Thursday, October 27, 2016.

PLV Seminar

Georgios Fainekos
Arizona State University

10-27-2016 15:30
ECCR 265

Beyond Requirements Falsification: Semi-Formal Methods and Tools for the Analysis of Cyber-Physical Systems

Abstract

Correct-by-design synthesis methods for Cyber-Physical Systems (CPS) are still in their infancy for CPS with complex physical dynamics. For that reason, a combination of design theories for simpler systems and/or ad-hoc design approaches are utilized. Hence, numerous design and implementation errors are discovered while CPS are operational in the field. Such errors can have catastrophic effects to human life and to the economy. Over the last few years, requirements guided falsification methods have proven to be a practical approach to the verification problem of industrial size CPS. However, requirements falsification is just one component of the necessary tools for the development of safe and reliable CPS. In this talk, Fainekos will provide an overview of his team's research in providing support for all the stages of the development for CPS, from formal requirements elicitation and mining to system conformance to on-line monitoring. Most of their methods have been implemented in a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). Finally, in this talk, he will demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive industry.

Biography

Georgios Fainekos is an associate professor at the School of Computing, Informatics and Decision Systems Engineering (SCIDSE) at Arizona State University (ASU). He is director of the Cyber-Physical Systems (CPS) Lab and he is currently affiliated with the NSF I/UCR Center for Embedded Systems (CES) at ASU. He received his PhD in Computer and Information Science in 2008 from the University of Pennsylvania, where he was affiliated with the GRASP laboratory. He holds a Diploma degree (BSc and MSc) in Mechanical Engineering from the National Technical University of Athens and an MSc degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU, he held a postdoctoral researcher position at NEC Laboratories America in the System Analysis and Verification Group. He is currently working on Cyber-Physical Systems and robotics. In particular, his expertise is on formal methods, logic, artificial intelligence, optimization and control theory. His research has applications on automotive systems, medical devices, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2013, Fainekos received the NSF CAREER award. He was also recipient of the SCIDSE Best Researcher Junior Faculty award for 2013 and of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. Two of his conference papers have been nominated for student best paper awards.

2016.10.26

Call for Ph.D. applicants for Fall 2016. Application deadline is December 15, 2015. Check out our latest recruiting talk from February 20, 2015.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; program synthesis; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL and PLDI. CS Admissions (deadline December 15, 2016) and ECEE Admissions (deadline January 15, 2016 but earlier for financial aid consideration).

2016.10.13

CUPLV authors Bor-Yuh Evan Chang and Matthew A. Hammer with collaborators have had papers accepted for presentation at POPL 2017 in January (Li et al. and ).

2016.08.26

CUPLV authors Bor-Yuh Evan Chang and Matthew A. Hammer have had a paper "A Vision for Online Verification-Validation" accepted for presentation at GPCE 2016 in November.

2015.06.17

Congratulations to Benno Stein for being awarded second place in the graduate student category at the PLDI Student Research Competition (SRC) for his project, "Goal-Directed Abstract Interpretation for JavaScript."

2016.06.14

CUPLV authors Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan have had a paper "Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants" accepted for presentation at SAS 2016 in September.

2016.05.20

CUPLV authors Hadi Ravanbakhsh and Sriram Sankaranarayanan have had a paper "Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework" accepted for presentation at EMSOFT 2016 in October.

2016.05.13

CUPLV faculty Matthew A. Hammer and Bor-Yuh Evan Chang have been awarded an NSF grant "Online Verification-Validation" with collaborator David Van Horn at the University of Maryland.

2016.05.06

CUPLV authors Michael Dooley, Fabio Somenzi, and Sergio Mover have had papers accepted for presentation at CAV 2016 in July (Dooley and Somenzi and Daniel et al.).

2016.04.19

Saeid Tizpaz Niari wins Second Prize in the Microsoft Open Source Challenge for his entry "CONfidentiality CERTifier: a Modeling and Verification Framework for Program Confidentiality using Z3".

2016.04.17

CUPLV authors Jedidiah McClurg and Pavol Černý and collaborators at Cornell have had a paper accepted for presentation at PLDI 2016 in June (McClurg et al.).

2016.04.13

Aditya Zutshi wins the Best Student Paper Award at HSCC 2016 for his paper "Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software" co-authored with Sriram Sankaranarayanan and collaborators.

Best Student Paper Award at HSCC 2016


            Aditya with his award!
Congratulations, Aditya!

2015.12.20

CUPLV authors Aditya Zutshi, Sriram Sankaranarayanan, and with collaborators have had a paper "Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software" accepted for presentation at HSCC 2016 in April.

2015.12.18

CUPLV authors Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at TACAS 2016 in April (Bouissou et al. and Chakarov et al.).

2015.11.01

Please consider applying or encourage your students and postdocs to apply for a tenure-track position in the Department of Computer Science (CS) and Department of Electrical, Computer, and Energy Engineering (ECEE) at the University of Colorado Boulder. We have multiple openings with one particular interest area in Computer Science being secure and reliable software systems. Applications will be evaluated beginning on November 9, 2015 with priority given to applications received by December 7, 2015, although applications will continue to be evaluated until the position is filled. Apply at http://www.jobsatcu.com/postings/109940 for CS and at https://www.jobsatcu.com/postings/107808 for ECEE.

Tenure-Track Position

The Department of Computer Science (CS) at the University of Colorado Boulder seeks applications for multiple tenure-track positions. The openings are targeted at the level of Assistant Professor, but experienced candidates may be considered for Associate or Full Professor. Research areas of particular interest include, but are not limited to, the areas of secure and reliable software systems (with an emphasis in software engineering and/or security), network science, scientific data analysis and visualization, computer systems as applied to autonomous and networked devices, and theoretical computer science. Our department values inclusive excellence and we seek candidates that understand the benefits that diversity brings to scientific innovation and who, through their work, develop technologies that impact a wide range of communities. Our department is also responsive to dual career situations.

Our vision of successful candidates are those who demonstrate the potential for excellence in both research and teaching, have a strong interest in interdisciplinary collaboration, and aim to lead a visible, externally funded research program. Candidates must have a Ph.D. in computer science or a related discipline and must show promise in their ability to develop an independent and internationally recognized research program. They must also display an ability, a record of excellence, and/or a commitment to teaching and working with undergraduate and graduate students of diverse backgrounds.

Applications will be evaluated beginning on November 9, 2015 with priority given to applications received by December 7, 2015, although applications will continue to be evaluated until the position is filled. Applications must include a cover letter specifying the applicant's areas of specialization and describing their interest in the Department of Computer Science at CU Boulder. Applications must also include a curriculum vita, statements of research and teaching interests, and names and contact information for three references. In their statements, candidates should describe and include specific examples of how their experience would contribute to the department's mission and values, including, but not limited to, their research record, pedagogical approaches, teaching content, mentoring and recruiting activities, community engagement, and experiences working with underrepresented communities.

The Department's research and education efforts interact broadly with many interdisciplinary programs and collaborators in the Boulder area, including national labs at NIST, NOAA, NREL, and NCAR, and CU Boulder research institutes including the ATLAS Institute, the BioFrontiers Institute, and the Institute for Cognitive Science. The Department has a long-standing partnership with the National Center for Women and IT and has faculty active in increasing the broadening of participation in computer science via their research, teaching, and service. The Department also has extensive ties with the thriving local tech community and inhabits a picturesque location in the foothills of the Rocky Mountains.

Applications are to be submitted on-line at http://www.jobsatcu.com/postings/109940.

The Department of Electrical, Computer, and Energy Engineering (ECEE) at the University of Colorado Boulder seeks outstanding candidates for up to three tenure-track faculty positions beginning August 2016. The openings are targeted at the level of Assistant Professor, but experienced candidates with outstanding credentials may be considered at any rank.

Hiring priority areas in ECEE include computer systems, next-generation networks, data analysis for complex systems, applied electromagnetics, RF/microwave engineering, power systems and electronics, integrated circuits, controls, nano-materials and systems, optics/photonics, and imaging. Exceptionally qualified candidates in other areas of electrical, computer, and energy engineering will be considered. Candidates involved in research bridging disciplines are highly encouraged to apply.

Candidates must have a Ph.D. in electrical engineering or related disciplines; they must have the ability to develop an independent research program, enthusiasm to work with other faculty in the department and dedication to teaching at all levels.

The department includes 2 University Distinguished Professors, 14 Full, 13 Associate, and 9 Assistant Professors. Faculty honors include 14 IEEE Fellows, 2 members of the US National Academy of Engineering, a Packard Fellow, a NSF Presidential Faculty Fellow and 10 NSF CAREER Award recipients. The ECEE program consists of about 350 undergraduate and 300 graduate students, and has averaged over $12.5 million in annual research grants. The department maintains close ties with local industry and national institutes/labs such as NIST, NREL, and NOAA.

Complete applications submitted by December 1, 2015 will receive full consideration, though applications received after this date will continue to be reviewed until the positions are filled. Applications must include a cover letter specifying the area of specialization, complete curriculum vitae, statement of research and teaching interests, and names and contact information of at least three references.

Applications are to be submitted on-line at https://www.jobsatcu.com/postings/107808.

2015.11.01

There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý on program analysis and program synthesis.

Postdoc Position


    The majestic, snow-covered Flatirons is a breathtaking backdrop with Old Main at the University of Colorado Boulder in the foreground. (Photo by Casey A. Cass/University of Colorado)
The Programming Languages and Verification Group at the University of Colorado Boulder (CUPLV) is looking for candidates for a postdoctoral research associate in the area of program analysis and program synthesis.

The position is on the Fixr project, a large project examining approaches to automatically mine, understand, and transfer bug fixes in large application frameworks, such as Android.

The ideal candidate has a background in the area of programming languages, software engineering and/or formal methods, as well as an enthusiasm for mentoring junior researchers.

The postdoctoral researcher would have the opportunity to lead this ambitious project that combines program analysis, probabilistic reasoning, and program synthesis. There will also be interactions with human-centered computing and big data engineering researchers on the interdisciplinary aspects of the project.

The position is for one to two years, with a possible extension for additional years. A transition plan to a research assistant professor position is possible for highly-qualified candidates. While not required, teaching opportunities will also be available. Compensation is highly competitive and commensurate with experience.

To apply, please send an email to Bor-Yuh Evan Chang with a CV and contact information for two to three references. Applications will be considered until the position is filled.

Our group has active projects in areas such as the following:

Boulder, located at the base of the Rocky Mountain foothills, is consistently awarded top-rankings for health, education, and quality of life. It is also home to a concentration of high-tech industry and its vibrant startup community. Located 30 miles from downtown Denver, there are convenient public transportation options between Boulder and the Denver metro area.

2015.11.01

Call for Ph.D. applicants for Fall 2016. Application deadline is December 15, 2015. Check out our latest recruiting talk from February 20, 2015.

Ph.D. Positions

We are looking for enthusiastic students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; language-based security; type systems; language design; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL and PLDI. CS Admissions (deadline December 15, 2016) and ECEE Admissions (deadline January 15, 2016 but earlier for financial aid consideration).

2015.10.15

Thomas Ball from Microsoft Research is visiting us on October 19-20, 2015. He is giving a CUPLV Seminar entitled "Recent Results in Automated Verification from Microsoft Research" at 9:30am in ECCR 150 on Tuesday, October 20, 2015.

PLV Seminar

Thomas Ball
Microsoft Research

10-20-2015 9:30
ECCR 150

Recent Results in Automated Verification from Microsoft Research

Abstract

In this talk, I’ll review recent results in automated verification from members of Microsoft Research, addressing problems such as: (1) whole program analysis using automated theorem provers; (2) analyzing open programs efficiently and precisely; (3) speeding up interprocedural verifiers through apriori program transformations.

This work is by Ankush Das, Shuvendu Lahiri, Akash Lal and Shaz Qadeer of Microsoft Research, along with their interns.

Biography

Thomas Ball is a research manager in the area of software engineering. His research interests are in how combinations of static/dynamic program analysis, model checking and theorem proving techniques can help improve the correctness and reliability of programs.

Hosted by Matthew A. Hammer.

2015.08.04

CUPLV authors Sam Blackshear, Bor-Yuh Evan Chang, Matthew A. Hammer, and Kyle Headley have had papers accepted for presentation at OOPSLA 2015 in October (Blackshear et al. and Hammer et al.).

2015.09.01

Kyle Headley comes in second at ICFP-SRC 2015 in the undergraduate category.

2015.06.01

CUPLV author Bor-Yuh Evan Chang with collaborators has had a paper "Shape Analysis for Unstructured Sharing" accepted for presentation at SAS 2015 in September.

2015.05.27

Mayur Naik from Georgia Tech is visiting us on May 28-29, 2015. He is giving a CUPLV Seminar entitled "Petablox: Declarative Program Analysis for Big Code" at 10:30am in DLC 1B70 on Friday, May 29, 2015.

PLV Seminar

Mayur Naik
Georgia Tech

05-29-2015 10:30
DLC 1B70

Petablox: Declarative Program Analysis for Big Code

Abstract

Most software development today leverages the world's massive collection of open source software. There is significant room for program analyses to similarly leverage Big Code, the collective knowledge amassed from analyzing existing programs, to automatically infer or predict salient behaviors and vulnerabilities in new programs. We present Petablox, a framework for automatically synthesizing use-cases of arbitrary declarative program analyses for Big Code tasks such as efficiently finding good abstractions, transferring analysis results across programs, and adapting analyses to user feedback. Despite their diversity, all these tasks entail solving large instances of MaxSAT, the maximum satisfiability problem which comprises a mix of hard (inviolable, logical) constraints and soft (violable, probabilistic) constraints. We describe demand-driven, compositional, and learning-based MaxSAT optimizations in Petablox for scaling these tasks to large code bases.

Biography

Mayur Naik is an Assistant Professor in Computer Science at Georgia Tech since 2011. His research interests are in programming languages and software engineering, with a current emphasis on program analysis techniques and systems for improving software quality and programmer productivity on modern computing platforms such as parallel, mobile, and cloud computing. He holds a Ph.D. in Computer Science from Stanford University (2007) and was a research scientist at Intel Labs, Berkeley from 2008 to 2011.

Hosted by Bor-Yuh Evan Chang.

2015.05.27

Sam Blackshear is defending his PhD on at 1:00pm in ECAE 199 on Thursday, May 28, 2015. His PhD is entitled "Flexible Goal-Directed Abstraction."

PLV Seminar

Sam Blackshear
University of Colorado Boulder

05-28-2015 13:00
ECAE 199

Flexible Goal-Directed Abstraction

Abstract

Static program analysis is a powerful technique for bug-finding, verification, and program understanding. Yet static analyses remain conspicuously absent from the toolbox of the average developer because they must abstract away details about concrete program behavior. Designing effective abstractions is tricky business: imprecise abstractions are inexpensive, but can be useless because they lose too much information about the program, whereas conventional wisdom states that precise abstractions are too expensive to scale.

This dissertation considers the problem of goal-directed static analysis, an intriguing domain where there is hope for defying the conventional wisdom about precise and scalable abstractions. In contrast to more traditional whole-program approaches that must apply precise abstractions to the entire program, goal-directed approaches have the potential to be much more tractable because they can focus the effort of the analysis on a single goal query.

There are two fundamental challenges in goal-directed analysis: (A) designing abstractions that are as flexible as possible so they can be specialized to the needs of the query and (B) using this flexibility wisely to achieve a better precision/scalability tradeoff in practice. This dissertation addresses these challenges by introducing goal-directed abstraction coarsening, a new approach to goal-directed analysis. Our approach works backward from the goal query using an abstraction that is as precise as possible by default, but can be coarsened in order to narrow the focus of the analysis and improve scalability. We meet Challenge A by introducing flexible coarsening-based techniques for store abstraction and control-flow abstraction. Our store abstraction precisely represents a small view of the store relevant to the query by combining a separation logic-based representation with a flow-insensitive points-to analysis. We present a general framework for flexible control-flow abstraction that allows the framework to coarsen the control-flow abstraction by jumping over irrelevant code. Finally, we meet Challenge B by presenting goal-directed analyses incorporating our flexible abstractions. Our analyses use programmers’ invariant-based reasoning and the structure of event-driven programs to recognize opportunities for coarsening that are likely to enhance scalability without losing precision. We have implemented these analyses and shown that they can achieve precise and scalable results for a variety of client analyses than cannot be handled effectively by previous techniques.

Committee: Bor-Yuh Evan Chang (chair), Pavol Černý, Mayur Naik, Sriram Sankaranarayanan, and Manu Sridharan.

Biography

Sam Blackshear earned a BA in Computer Science and Philosophy from Williams College in 2010. He is interested in static program analysis, verification, and type systems. He has interned at Microsoft Research India, Microsoft Research Redmond, and Facebook London. He is a recipient of the 2013-2014 CU CS Outstanding Research Award, the 2015 Ralph J. Slutz Excellence Award, and a 2014-2015 Facebook Fellowship. He will work on static analysis and developer tools at Facebook after graduating.

2015.05.18

There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý on program analysis and program synthesis.

Postdoc Position


    The majestic, snow-covered Flatirons is a breathtaking backdrop with Old Main at the University of Colorado Boulder in the foreground. (Photo by Casey A. Cass/University of Colorado)
The Programming Languages and Verification Group at the University of Colorado Boulder (CUPLV) is looking for exceptional candidates for a postdoctoral research associate in the area of program analysis and program synthesis.

The position is on the Fixr project, a large project examining approaches to automatically mine, understand, and transfer bug fixes in large application frameworks, such as Android.

The ideal candidate has a strong background in the area of programming languages, software engineering and/or formal methods, as well as an enthusiasm for mentoring junior researchers.

The postdoctoral researcher would collaborate with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý and have the opportunity to lead this ambitious project that combines program analysis, probabilistic reasoning, and program synthesis. There will also be interactions with human-centered computing and big data engineering researchers on the interdisciplinary aspects of the project.

The position is for one to two years, with a possible extension for additional years. A transition plan to a research assistant professor position is possible for highly-qualified candidates. While not required, teaching opportunities will also be available. Compensation is highly competitive and commensurate with experience.

To apply, please send an email to Bor-Yuh Evan Chang with a CV and contact information for two to three references. Applications will be considered until the position is filled.

Our group has active projects in areas such as the following:

Boulder, located at the base of the Rocky Mountain foothills, is consistently awarded top-rankings for health, education, and quality of life. It is also home to a concentration of high-tech industry and its vibrant startup community. Located 30 miles from downtown Denver, there are convenient public transportation options between Boulder and the Denver metro area.

The University of Colorado is an Equal Opportunity Employer committed to building a diverse workforce. We encourage applications from women, minorities candidates, people with disabilities, and veterans.

2015.04.26

Matthew A. Hammer joins CUPLV as an assistant professor of computer science in Fall 2015. Welcome, Matt!

2015.04.25

CUPLV author Pavol Černý has had papers accepted for presentation at CAV 2015 in July (Alur et al. and Černý et al.).

2015.04.25

CUPLV authors Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang have had a paper "Droidel: A General Approach to Android Framework Modeling" accepted for presentation at SOAP 2015 in June.

2015.04.21

CUPLV faculty Pavol Černý, Bor-Yuh Evan Chang, Sriram Sankaranarayanan have been awarded a DARPA grant "STAC: Auditr: Securing Space/Time Defenses in Java Bytecode" with collaborators John Black at CU, Işıl Dillig and Marijn J. H. Heule at UT Austin, and Henny Sipma at Kestrel Technology.

2015.04.21

CUPLV authors Youngsung Kim and Pavol Černý with collaborators have had a paper "Performance Search Engine Driven by Prior Knowledge of Optimization" accepted for presentation at ARRAY 2015 in June.

2015.04.16

Ashutosh Trivedi from IIT Bombay is visiting us on April 17, 2015. He is giving a CUPLV Seminar entitled "Decidable Subclasses of Multi-Mode Systems" at 1:00pm in KOBL 235 on Friday, April 17, 2015.

PLV Seminar

Ashutosh Trivedi
Indian Institute of Technology Bombay

04-17-2015 13:00
KOBL 235

Decidable Subclasses of Multi-Mode Systems (Schedulability, Reachability, and Related Problems)

Abstract

Hybrid automata are a natural and expressive formalism to model systems that exhibit both discrete and continuous behavior. However, the applications of hybrid automata in analyzing cyber-physical systems have been rather limited due to undecidability of simple verification problems such as reachability. This drawback of hybrid automata has fueled the investigation of the so-called compositional methodology to design complex system by sequentially composing well-understood lower-level components. This methodology has, for example, been used in the context of the motion planning problem for mobile robots, where the task is to move a robot along a pre-specified trajectory with arbitrary precision by sequentially composing a set of well-studied simple motion primitives, such as “move left”, “move right” and “go straight”. In this talk, we summarize some of our recent results related to efficient solution of motion planning problem for systems whose motion primitives are given as constant-rate vectors with uncertainties.

Hosted by Sriram Sankaranarayanan.

2015.02.16

Prospective Ph.D. students visit February 20. Welcome!

2015.02.11

CUPLV authors Jedidiah McClurg and Pavol Černý and collaborators at Cornell have had a paper accepted for presentation at PLDI 2015 in June (McClurg et al.).

2015.01.29

CUPLV author Bor-Yuh Evan Chang have a paper appearing in CACM (Livshits et al.).

2015.01.28

CUPLV student Sam Blackshear receives the 2015 Ralph J. Slutz Student Excellence Award.

2014.12.16

CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Pavol Černý with collaborators have had papers accepted for presentation at ESOP 2015 in April (Cox et al. and Černý et al.).

2014.11.30

Leonid Ryzhyk from Carnegie Mellon University is visiting us on December 5, 2014. He is giving a CUPLV Seminar entitled "Automatic Device Driver Synthesis" at 4:00pm in ECOT 831 on Friday, December 5, 2014.

PLV Seminar

Leonid Ryzhyk
Carnegie Mellon University

12-05-2014 16:00
ECOT 831

Automatic Device Driver Synthesis

Abstract

Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit, called Termite. Termite is the first tool to combine the power of automation with the flexibility of conventional development. It is also the first practical synthesis tool based on abstraction refinement. Finally, it is the first synthesis tool to support automated debugging of input specifications. I will explain the main principles behind the tool and give a brief demo of its capabilities.

Biography

Leonid Ryzhyk is a postdoctoral researcher in the Carnegie Mellon University School of Computer Science. Leonid's research focuses on applying rigorous formal techniques to the design, implementation, and verification of operating systems. He received his PhD from the University of New South Wales in 2010. Prior to joining CMU, Leonid worked as a researcher at NICTA and a postdoctoral fellow at the University of Toronto.

Hosted by Pavol Černý.

2014.11.30

Manu Sridharan from Samsung Research America is visiting us on December 3, 2014. He is giving a CUPLV Seminar entitled "MemInsight: Platform-Independent Memory Profiling for JavaScript" at 4:00pm in ECCR 116 on Wednesday, December 3, 2014.

PLV Seminar

Manu Sridharan
Samsung Research America

12-03-2014 16:00
ECCR 116

MemInsight: Platform-Independent Memory Profiling for JavaScript

Abstract

JavaScript programs tend to suffer from memory issues that can either hurt performance, or worse, make programs crash due to slow exhaustion of memory. We present a new memory profiling tool MemInsight for JavaScript applications, including web applications. MemInsight is platform independent: it employs source-code instrumentation to generate a trace of memory allocations and accesses, and it uses standard browser features to track precise information for DOM (document object model) objects. The information thus collected enables detailed, time-varying analysis of memory behavior, including that of DOM objects.

We describe several client analyses built into MemInsight. For instance, it points out situations in which there may be a memory leak, and it reports opportunities for replacing dynamic allocation with stack allocation. MemInsight is extensible to custom analyses as well. Our experimental evaluation showed that our client analyses found interesting memory issues in several publicly available apps, and that MemInsight had reasonable overhead.

Biography

Manu Sridharan is a researcher at Samsung Research America in the area of programming languages and software engineering. He received his PhD from the University of California, Berkeley in 2007. His dissertation focused on refinement-based program analysis tools. Since then, he has done research on a variety of topics in static analysis, dynamic analysis, and software engineering. He worked at IBM Research from 2008–2013. For further details, see http://manu.sridharan.net.

Hosted by Bor-Yuh Evan Chang.

2014.11.30

Nina Narodytska from Carnegie Mellon University is visiting us on December 1, 2014. She is giving a CUPLV Seminar entitled "SAT-based Techniques for Reactive Synthesis" at 3:00pm in ECEE 1B55 on Monday, December 1, 2014.

PLV Seminar

Nina Narodytska
Carnegie Mellon University

12-01-2014 15:00
ECEE 1B55

SAT-based Techniques for Reactive Synthesis

Abstract

Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. I will present a new game solving method that works by exploring a subset of all possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided backtracking search, inspired by the RaReQs QBF solver, to identify a subset of runs that are sufficient to consider to solve the game. Our search procedure performs learning from both players' failures, gradually shrinking winning regions for both players. In addition, it allows extracting compact winning/spoiling strategies using interpolation procedures. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems. Our approach outperforms state-of-the-art BDD solvers on some families of benchmarks. We demonstrated that our strategy extraction procedure is efficient and introduces low overhead on top of the main solver.

Biography

Nina Narodytska is a visiting researcher in the Carnegie Mellon University School of Computer Science. She received her PhD from the University of New South Wales in 2011. Nina works on developing efficient algorithms for decision and optimization problems. She was named one of "AI's 10 to Watch" young researches in the field of AI. She also received an Outstanding Paper Award at AAAI 2011 and an outstanding program committee member award at the Australasian Joint Conference on Artificial Intelligence 2012. Her EvaMaxSAT Solver is a winner of the Ninth Evaluation of Max-SAT Solvers in 2014.

Hosted by Pavol Černý.

2014.10.24

Devin Coughlin comes in second at the SPLASH-SRC 2014.

2014.10.16

Aditya Zutshi and Sriram Sankaranarayanan receive the best paper award for their paper "Multiple Shooting, CEGAR-based Falsification for Hybrid Systems" at EMSOFT 2014.

EMSOFT 2014 Best Paper Award

The conference on embedded software was held in New Delhi this year as part of a broader series of conferences called Embedded Systems week (ESWeek). 120 papers were submitted, 29 were accepted, and one paper was given this award. More details at http://esweek.acm.org/bestpaper.shtml.

2014.10.15

Please consider applying or encourage your students and postdocs to apply for a tenure-track position in the Department of Computer Science at the University of Colorado Boulder. We have multiple openings with one particular interest area being secure and reliable software systems. Applications will be evaluated beginning on December 1, 2014, will continue until the position is filled, and are to be submitted on-line at http://www.jobsatcu.com/postings/89652.

Tenure-Track Position

The Department of Computer Science (CS) at the University of Colorado Boulder seeks outstanding candidates, for multiple tenure-track positions. The openings are targeted at the level of Assistant Professor, although exceptional candidates at higher ranks may be considered. Research areas of particular interest include the areas of secure and reliable software systems, numerical optimization and high-performance scientific computing, and network science and machine learning.

Candidates for these positions must demonstrate excellence in both research and teaching, have a strong interest in interdisciplinary collaboration, and aim to lead a highly visible, externally funded research program. Candidates must have a Ph.D. in computer science or a related discipline and must show promise in their ability to develop an independent and internationally recognized research program. They must also display a demonstrated commitment to teaching and working with both undergraduate and graduate students.

Applications will be evaluated beginning on December 1, 2014 and will continue until the position is filled. Applications must include a cover letter specifying the applicant’s areas of specialization and describing their interest in the Department of Computer Science at CU Boulder. Applications must also include a curriculum vitae, statements of research and teaching interests, and names and contact information for three references.

The Department’s research and education efforts interact broadly with many interdisciplinary programs and collaborators in the Boulder area, including national labs at NIST, NOAA, NREL, and NCAR, and CU Boulder research institutes including the BioFrontiers Institute and the Institute for Cognitive Science. The Department also has extensive ties with the thriving local tech community and inhabits a picturesque location in the foothills of the Rocky Mountains.

The University of Colorado Boulder is an Equal Opportunity Employer committed to building a diverse workforce. We encourage applications from women, racial and ethnic minorities, individuals with disabilities and veterans. Alternative formats of this ad can be provided upon request for individuals with disabilities by contacting the ADA Coordinator at hrada@colorado.edu.

The University of Colorado Boulder is committed to providing a safe and productive learning and living community. To achieve that goal, we conduct background investigations for all final applicants being considered for employment. Background investigations include reference checks, a criminal history record check, and when appropriate, a financial and/or motor vehicle history.

Applications must be submitted on-line at http://www.jobsatcu.com/postings/89652.

2014.10.02

Christos Dimoulas from Harvard is visiting us on October 7, 2014. He is giving a CUPLV Seminar entitled "Behavioral contracts and security" at 11:00am in ECCR 151 on Tuesday, October 7, 2014.

PLV Seminar

Christos Dimoulas
Harvard University

10-07-2014 11:00
ECCR 151

Behavioral contracts and security

Abstract

Behavioral contracts are a widely used specification tool for software components, which enrich interface information with logical assertions. The rigorous enforcement of contracts provides to programmers precise guarantees about a program's execution, and offers useful feedback for debugging upon contract violations. However, almost all of research on contracts focuses on contracts as a specification tool for partial correctness of programs and ignores another vital requirement of modern software; security.

In this talk, I will demonstrate how contracts can specify and enforce security policies. Specifically, I will focus on two applications of contracts in capability-based security. First, I will describe Shill; a secure shell scripting language where contracts specify and enforce policies about which OS resources scripts intend to use and how they use them. This way, Shill's contracts help script authors and users to adhere to the principle of least privilege. Second, I will present a contract system that complements the contract system of Shill by describing and enforcing declarative policies for the flow of capabilities between components. This manner, components can specify not only what capabilities they require from their users, but also how they intend to share these capabilities with other components.

Biography

Christos Dimoulas is a Postdoctoral Fellow in Computer Science at the School of Engineering and Applied Sciences of Harvard University working with Stephen Chong and his group. Before coming to Harvard, Christos completed a PhD in Computer Science at the College of Computer and Information Science of Northeastern University under the supervision of Matthias Felleisen. Christos is interested in the design and semantics of programming languages. More specifically, his goal is to develop programming languages technology that facilitates the construction of secure and robust component-based software systems.

2014.09.24

CUPLV faculty Bor-Yuh Evan Chang, Pavol Černý, Sriram Sankaranarayanan have been awarded a DARPA grant "MUSE: Mining and Understanding Bug Fixes to Address Application-Framework Protocol Defects" with collaborators Kenneth M. Anderson and Tom Yeh.

2014.09.12

Aleksandar Chakarov wins the Radhia Cousot Young Researcher Best Paper Award at SAS 2014 for his paper "Expectation Invariants for Probabilistic Program Loops as Fixed Points" co-authored with Sriram Sankaranarayanan.

Radhia Cousot Young Researcher Best Paper Award


    Aleks Chakarov with his award!
Congratulations, Aleks!

2014.07.10

There is a postdoctoral research associate position open with the opportunity to work with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý. Highly-qualified candidates may be considered for a research assistant professor position.

Postdoc Position


    The majestic, snow-covered Flatirons is a breathtaking backdrop with Old Main at the University of Colorado Boulder in the foreground. (Photo by Casey A. Cass/University of Colorado)
The Programming Languages and Verification Group at the University of Colorado Boulder (CUPLV) is looking for exceptional candidates for a postdoctoral research associate in the area of program analysis and program synthesis.

The ideal candidate has a very strong background in the general area of programming languages and verification.

The postdoctoral researcher would collaborate with Profs. Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Pavol Černý. To apply, please send an email to any of us with CV and contact information for two or three references.

Our group has active projects in areas such as the following:

The position is for one year, with a possible extension for additional years. Highly-qualified candidates may be considered for a research assistant professor position. Compensation is highly competitive and commensurate with experience.

The University of Colorado is an Equal Opportunity Employer committed to building a diverse workforce. We encourage applications from women, minorities candidates, people with disabilities, and veterans.

Boulder, located at the base of the Rocky Mountain foothills, is consistently awarded top-rankings for health, education, and quality of life. It is also home to a concentration of high-tech industry and its vibrant startup community.

2014.07.10

Eric Schkufza from Stanford is visiting us on July 15, 2014. He is giving a CUPLV Seminar entitled "Stochastic Optimization of x86_64 Binaries" at 11:00am in KOBL 300 on Tuesday, July 15, 2014.

PLV Seminar

Eric Schkufza
Stanford University

07-15-2014 11:00
KOBL 300

Stochastic Optimization of x86_64 Binaries

Abstract

The optimization of short sequences of loop-free fixed-point x86_64 code sequences is an important problem in high-performance computing. Unfortunately, the competing constraints of transformation correctness and performance improvement often force even special purpose compilers to produce sub-optimal code. We show that by encoding these constraints as terms in a cost function, and using a Markov Chain Monte Carlo sampler to rapidly explore the space of all possible programs, we are able to generate aggressively optimized versions of a given target program. Beginning from binaries compiled by gcc -O0, we are able to produce provably correct code sequences that either match or outperform the code produced by gcc -O3, and in some cases expert hand-written assembly.

Because most high-performance applications contain floating-point computations, we extend our technique to this domain and show a novel approach to trading full floating-point precision for further increases in performance. We demonstrate the ability to generate reduced precision implementations of Intel's handwritten C numerics library that are up to six times faster than the original code, and achieve end-to-end speedups of over 30% on a direct numeric simulation and a ray tracer. Because optimizations that contain floating-point computations are not amenable to formal verification using the state of the art, we present a technique for characterizing maximum error and providing strong evidence for correctness.

Biography

Eric Schkufza is a PhD candidate at Stanford University (a few signatures away from graduating!) working with Professor Alex Aiken. He is interested in applying machine learning and stochastic search techniques to the design of optimizing compilers.

2014.06.27

CUPLV authors Hadi Ravanbakhsh, Aditya Zutshi, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at EMSOFT 2014 in October (Ravanbakhsh and Sankaranarayanan, and Zutshi et al.).

2014.06.01

CUPLV authors Aleksandar Chakarov, Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at SAS 2014 in September (Chakarov and Sankaranarayanan, Cox et al., and Toubhans et al.).

2014.04.21

CUPLV student Sam Blackshear receives the 2013-2014 CU CS Outstanding Research Award.

2014.04.18

CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan have had a paper "QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers" accepted for presentation at CAV 2014 in July.

2014.02.19

S-Taliro developed by Sriram Sankaranarayanan and collaborators receives press coverage in Embedded Computing Design.

2014.02.19

Prospective Ph.D. students visit February 21. Welcome!

2014.02.03

Sam Blackshear is one of only eleven winners of a 2014-2015 Facebook Graduate Fellowship!

2014.02.05

CUPLV author Sam Blackshear with collaborators have had a paper "Verification Modulo Versions: Towards Usable Verification" accepted for presentation at PLDI 2014 in June.

2014.01.22

Devin Coughlin presenting "Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants" at POPL 2014 today.

2013.12.01

CUPLV graduate student Aleksandar Chakarov and undergraduate student Paul Givens receive the 2013 Ralph J. Slutz Student Excellence Award.

2013.10.01

CUPLV authors Devin Coughlin, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at POPL 2014 in January (Coughlin and Chang and Jeannet et al.).

2013.06.08

Eight CUPLV papers are being presented this summer: PLDI 2013 June 16-22 [Blackshear et al., Sankaranarayanan et al., Blackshear and Lahiri], LICS 2013 June 25-28 [Chaudhuri et al.], ECOOP 2013 July 1-5 [Cox et al.], and CAV 2013 July 13-19 [Černý et al., Chakarov and Sankaranarayanan, Chen et al.].

2013.05.21

Arlen Cox wins a Chateaubriand Fellowship in Science, Technology, Engineering, and Mathematics from the Embassy of France in the United States to study and conduct research in France.

2013.05.07

The artifact supplementing "QUIC Graphs: Relational Invariant Generation for Containers" has been validated and has received the distinguished artifact award at ECOOP 2013!

2013.03.25

Arlen Cox named a 2013-2014 Facebook Graduate Fellowship Finalist.

2013.03.06

CUPLV authors Pavol Černý, Aleksandar Chakarov, and Sriram Sankaranarayanan with collaborators have had papers accepted for presentation at CAV 2013 in July (Černý et al., Chakarov and Sankaranarayanan, and Chen et al.).

2012.03.04

CUPLV authors Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan have had a paper "QUIC Graphs: Relational Invariant Generation for Containers" accepted for presentation at ECOOP 2013 in July.

2013.03.04

Submit Analyzer Pearls to TAPAS 2013!

2013.02.21

Prospective Ph.D. students visit February 22. Welcome!

2013.02.04

CUPLV authors Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Aleksandar Chakarov with collaborators Manu Sridharan, Sumit Gulwani, and Shuvendu Lahiri have had papers accepted for presentation at PLDI 2013 in June (Blackshear et al., Sankaranarayanan et al., and Blackshear and Lahiri).

2013.01.31

Nathan Lapinksi and Sriram Sankaranarayanan have had their poster accepted to the SIGCSE 2013 Student Research Competition.

2013.01.31

Paul Givens, Aleksandar Chakarov, Sriram Sankaranarayanan, and Tom Yeh have had their paper accepted for presentation at ICSE 2013 (New and Emerging Results Track) in May.

2013.01.23

Sumit K. Jha from University of Central Florida is visiting us on January 24, 2013. He is giving a Computer Science Colloquium entitled "Validation and Parameter Discovery for Stochastic Computational Models from Behavioral Specifications" at 3:30pm in ECCR 265 on Thursday, January 24, 2013.

PLV Seminar

Sumit K. Jha
University of Central Florida

01-24-2013 15:30
ECCR 265

Validation and Parameter Discovery for Stochastic Computational Models from Behavioral Specifications

Abstract

The success of high-performance computing has facilitated the rapid development of increasingly complex models of natural and engineered systems by biologists, physicists, chemists, and even financial engineers. While the development of such models requires considerable domain knowledge and arguably little knowledge of the science of computing itself, we survey a key problem in computational modeling that cuts across boundaries of scientific disciplines and motivates the development of new massively parallel high-performance algorithms: the validation and parameter discovery for stochastic computational models.

Biography

Sumit K. Jha is an Assistant Professor and the Charles Millican Faculty Fellow with the Computer Science Department at the University of Central Florida, Orlando. He received his Ph.D. in Computer Science at Carnegie Mellon University. Before joining Carnegie Mellon, Dr. Jha graduated with B.Tech (Honors) in Computer Science and Engineering from the Indian Institute of Technology Kharagpur. His current research interests include automated verification and synthesis of stochastic and hybrid systems with emphasis on applications to computational finance and biochemical modeling. Dr. Jha has also worked on more traditional formal validation and machine learning problems at Microsoft Research, General Motors and INRIA, France. Dr. Jha also holds a Certificate in Quantitative Finance and is a member of the Alpha Quant Club - a network of academicians and industry leaders interested in mathematical finance.

2012.11.13

Jeffrey Sarnat from Twitter is visiting us on November 13, 2012. He is giving a Computer Science Colloquium entitled "Getting Off the Monorail or: How Twitter Learned to Stop Worrying and Love Monads" at 3:30pm in ECCR 265 on Thursday, November 13, 2012.

PLV Seminar

Jeffrey Sarnat
Twitter

11-13-2012 15:30
ECCR 265

Getting Off the Monorail or: How Twitter Learned to Stop Worrying and Love Monads

Abstract

Twitter is one of the most heavily trafficked sites on the internet, with over 140 million active users and serving over 400 million Tweets per day. Historically, nearly all of Twitter's traffic has been served by a monolithic application written in Ruby on Rails, referred to internally as "the monorail." Although Twitter has seen remarkable growth in its six years of existence, scaling this monolithic architecture has proved to be both error-prone and expensive, not only in terms of computational efficiency, but in terms of developer efficiency as well.

More recently, Twitter has begun the process of replacing the monorail with a Services Oriented Architecture (SOA), where the services are JVM processes--mostly written in Scala--that communicate with one-another asynchronously over a network connection. Naively written, asynchronous code is often both tedious to write and difficult to reason about; at Twitter, the asynchronous code implementing Scala services is both simple and beautiful, thanks in large part to an internally-developed, open-source library called Finagle.

In this talk, I will attempt to explain how Finagle's strong grounding in programming language theory has facilitated this transition to an SOA, and how Scala's advanced features allow for a library as expressive as Finagle to have been written in the first place.

Biography

Jeffrey Sarnat (B.S. in Computer Science., CMU 2002, Ph.D. in Computer Science, Yale 2010) is a former programming languages researcher who currently works for Twitter on a team that builds large scale distributed systems. He enjoys candlelit dinners and long walks on the beach. Follow him on Twitter as @Eigenvariable.

2012.10.28

Carl Friedrich Bolz visits October 29-November 2.

2012.10.02

CUPLV author Pavol Černý has had a paper "Quantitative Abstraction Refinement" accepted for presentation at POPL 2013 in January.

2012.09.30

Pavol Černý joins the University of Colorado Boulder (CU-Boulder) and CU Programming Languages and Verification (CUPLV) as an Assistant Professor of Electrical, Computer, and Energy Engineering (ECEE) in January 2013.

2012.09.27

Sriram Sankaranarayanan is giving a Computer Science Colloquium entitled "Finding Falsifications in Complex Cyber-Physical Systems" at 3:30pm in ECCR 265 on Thursday, September 27, 2012.

PLV Seminar

Sriram Sankaranarayanan
University of Colorado Boulder

09-27-2012 15:30
ECCR 265

Finding Falsifications in Complex Cyber-Physical Systems

Abstract

Cyber-Physical Systems (CPS) combine discretely evolving computational components with a continuously changing physical world. Examples of CPS include safety-critical systems that control airplanes, automobiles, power plants and implantable medical devices. Assuring the safety of these systems requires techniques that transcend the limited coverage provided by testing/simulation. Even though impressive progress has been achieved with symbolic formal verification techniques for linear systems, the verification of non-linear, industrial scale CPS designs remains a distant goal.

In this talk, I present a simple yet effective approach to automatically searching for property violations in non-linear systems. Our approach defines the notion of robustness metrics over traces that can be used to measure distances between simulation traces and properties expressed in temporal logics. As a result, robustness metrics can naturally quantify how "close" a particular simulation of the system is to violating a property of interest. By treating robustness metrics as an objective function to minimize over the simulation traces of the system, we can use many off-the-shelf global optimization techniques to effectively steer the simulations towards a falsification of the property being considered.

Despite the lack of strong formal guarantees, we find that robustness-guided falsification is a promising approach to searching for property violations in complex systems. We present the S-Taliro tool, an implementation of our approach to reason about properties of non-linear systems modeled as Simulink/Stateflow diagrams. We present two interesting case studies using S-Taliro, including a risk analysis of insulin infusion pump usage by diabetic patients that models the software in the pump in conjunction with the dynamics of insulin/glucose regulatory system.

Joint work with Georgios Fainekos (Arizona State).

Biography

Sriram Sankaranarayanan is an Assistant Professor of Computer Science at the University of Colorado Boulder. His research interests include techniques for verifying programs and cyber-physical systems. Sriram obtained a Ph.D. in 2005 from Stanford University. Subsequently he worked as a research staff member at NEC research labs in Princeton, NJ. He has been on the faculty at CU-Boulder since 2009. Sriram has been the recipient of awards including the Siebel Scholarship (2005), the CAREER award from NSF (2009) and the Dean's award for outstanding junior faculty for the College of Engineering at CU-Boulder (2012).

2012.09.25

Call for Ph.D. applicants for Fall 2013. Application deadline is December 15, 2012. Check out our latest recruiting talk from February 25, 2011.

Ph.D. Positions

We are looking for strong students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; language-based security; type systems; language design, compilation, and analysis for dynamic, web languages; performance analysis of data center-scale systems; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL and PLDI. CS Admissions (deadline December 15, 2012) and ECEE Admissions (deadline February 1, 2013 but earlier for financial aid consideration).

2012.09.19

CUPLV goes to MVD 2012 September 20-21.

2012.07.30

Xavier Rival visits July 30-August 16.

2012.07.19

Devin Coughlin is presenting the paper "Measuring Enforcement Windows with Symbolic Trace Interpretation: What Well-Behaved Programs Say" at ISSTA 2012 on July 19.

2012.07.15

Eric Goubault and Sylvie Putot visit July 16-20.

2012.06.21

Congratulations to Michael Vitousek for being awarded third place at the Programming Language Design and Implementation (PLDI) Student Research Competition (SRC) for his project: Gradual Typing with Efficient Object Casts.

2012.06.30

Franjo Ivančić from NEC Laboratories in Princeton, New Jersey is visiting us on July 2, 2012. Franjo is giving a talk at 2:00pm in ECOT 832 on Monday, July 2, 2012.

PLV Seminar

Franjo Ivančić
NEC Laboratories

07-02-2012 14:00
ECOT 832

Program Analysis for C++

Abstract

Program analyzes have been successful in finding serious program defects such as NULL pointer accesses or buffer overflows in programs written in C. However, industry relies heavily on object-oriented languages, such as Java and C++. This talk presents our recent advances in static analysis for C++. It focuses on C++ specific difficulties such as multiple inheritance, conversion from C++ strings to C strings and vice versa, and C++ exception semantics.

Biography

Franjo Ivančić is currently a Senior Research Staff Member at NEC Laboratories America in Princeton, NJ. Prior to joining NEC, he received his Ph.D. and MSE degrees in Computer and Information Science from the University of Pennsylvania in Philadelphia, PA. Earlier, he received his diploma (Dipl.-Inform.) degree from the Rheinische Friedrich-Wilhelms-University in Bonn, Germany, for his research performed at the Fraunhofer Institute in St. Augustin, Germany. His areas of research include software verification, model checking, formal modeling and analysis of hybrid systems, and design automation for embedded software. He received the Morris and Dorothy Rubinoff dissertation award from the University of Pennsylvania.

2012.06.11

Swarat Chaudhuri visits June 12.

2012.05.31

P.S. Thiagarajan from National University of Singapore is visiting us on June 4-5, 2012. He is giving a talk at 2:00pm in ECOT 831 on Monday, June 4, 2012.

PLV Seminar

P.S. Thiagarajan
National University of Singapore

06-04-2012 14:00
ECOT 831

Probabilistic Approximation and Analysis Bio-pathways Dynamics

Abstract

A system of Ordinary Differential Equations (ODEs) is often used to model the dynamics of a bio-chemical network. Such systems are difficult to analyze. To get around this, we construct a discrete probabilistic approximation of the ODE dynamics as a dynamic Bayesian network. Consequently, pathway properties can be analyzed using standard Bayesian inference techniques. Apart from testing our method on ODEs models drawn from the biomodels data base, we have used our technique in a combined computational and experimental study of the human complement system under inflammation conditions. Our results are very encouraging in terms of accuracy and efficiency. Finally, we have extended the scalability of our approach via a GPU implementation.

Biography

P.S. Thiagarajan received his B.Tech (Electrical Engineering) from the Indian Institute of Technology (IIT), Madras (1970) and his Ph.D. in Computer Science from Rice university, Houston, Texas, USA (1973). He is currently a Professor of Computer Science at the National University of Singapore.

He has held appointments at the Project MAC (the predecessor of the current Laboratory for Computer Science), Massachusetts Institute of Technology (MIT) (1973-1975), Gesellschaft fuer Mathematik und Datenverarbeitung, St. Augustin, Germany (1975-83), Aarhus University, Denmark (1983-86), Indian Institute of Mathematical Sciences, Chennai, India (1986-89) and the Chennai Mathematical Institute (1989-).

He has served as a member of the editorial boards of the journals Theoretical Computer Science and the International Journal on Foundations of Computing . He served two terms (1997 - 2003) as a member of the Governing Council of the European Association for Theoretical Computer Science (EATCS). He is a Fellow of the Indian Academy of Sciences and the Indian National Academy of Sciences.

His current research interests are: System-level design and analysis methods for real time embedded systems and computational systems biology.

2012.05.21

Paper accepted to SAS 2012 (by Sánchez et al.).

2012.04.20

Paper accepted to ISSTA 2012 (by Coughlin et al.).

2012.03.27

Arlen Cox is presenting the paper "A Bit Too Precise? Bounded Verification of Quantized Digital Filters" at TACAS 2012 on March 27.

2012.03.23

3 papers with CUPLV authors accepted to CAV 2012 (by Hassan et al., Zutshi et al., and Berdine et al.)

2012.02.23

Prospective Ph.D. students visit February 24.

2012.02.02

Bertrand Jeannet and Peter Schrammel from INRIA Rhône-Alpes in Grenoble, France are visiting us for two weeks from February 6, 2012 to February 17, 2012. Bertrand is giving a talk at 3:30pm in ECOT 831 on Friday, February 10, 2012, and Peter is presenting at 3:30pm in ECOT 831 on Friday, February 17, 2012.

PLV Seminar

Peter Schrammel
INRIA Rhône-Alpes

02-17-2012 15:30
ECOT 831

Towards the Verification of Hybrid Data-Flow Languages

Abstract

Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages, like Simulink, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. In this talk we first briefly present Zelus, a synchronous data-flow language extended with ordinary differential equations. Then we propose a sound translation from a Zelus-like hybrid data-flow formalism to logico-numerical hybrid automata discussing various zero-crossing semantics and the extent to which the original semantics is preserved. At last we sketch how existing continuous reachability analysis methods can be applied to logico-numerical hybrid automata.

PLV Seminar

Bertrand Jeannet
INRIA Rhône-Alpes

02-10-2012 15:30
ECOT 831

The BDDAPRON Logico-Numerical Abstract Domain Library

Abstract

We describe BDDAPRON, a freely available library dedicated to the static analysis of finite-type and numerical variables.

BDDAPRON provides ready-to-use logico-numerical abstractions for combinations of finite-type and numerical variables, as well as powerful symbolic manipulations of expressions.

Algorithmically, BDDAPRON combines BDD techniques (using the CUDD library) with numerical abstract domains provided by the APRON library. We describe the principles behind this combination and the various available options for the computation of abstract transfer functions.

At last, we present some applications of the BDDAPRON abstract domain to program verification, including recursive program with pointers.

2012.01.25

Neelam Agrawal, Devin Coughlin, Arlen Cox, and Erik Silkensen finalists at the POPL 2012 Student Lightning Talks.

2011.11.04

Best paper at FMCAD 2011 goes to "An Incremental Approach to Model Checking Progress Properties".

2011.11.04

Two tenure-track positions open. Evaluation begins December 6, 2011.

Faculty Positions (Two Openings)

University of Colorado Boulder: Department of Electrical, Computer, and Energy Engineering (ECEE) seeks outstanding candidates for two tenure-track positions in computer systems. The openings are targeted at the level of Assistant Professor, but experienced candidates with outstanding credentials may be considered for Associate or Full Professor.

Candidates interested in rigorous and innovative approaches to the design and analysis of complex computing systems (from embedded and cyberphysical to large-scale distributed systems) should apply. We seek candidates with background in programming languages, concurrency, security, formal methods, verification, or system engineering. Preference will go to researchers whose work spans multiple areas.

The positions will help shape the cooperation with the Department of Computer Science on computing systems.

Candidates must have a Ph.D. in electrical engineering, computer engineering, computer science, or related discipline; they must have the ability to develop an independent research program, and enthusiasm for working with undergraduate and graduate students.

The University of Colorado is an Equal Opportunity Employer committed to building a diverse workforce. We encourage applications from women, minorities candidates, people with disabilities, and veterans.

Applications will be evaluated starting December 6, 2011 and until the positions are filled.

Applications must include a letter of application specifying the desired position and area of specialization, complete curriculum vitae, statements of research and teaching interests, and names and contact information of three references. Applications must be submitted on-line at http://www.jobsatcu.com/ using posting number #815103 (computer systems). Additional information is available at that site.

2011.11.04

Call for Ph.D. applicants for Fall 2012. Application deadline is December 15, 2011. Check out our latest recruiting talk from February 25, 2011.

Ph.D. Positions

We are looking for strong students to join our diverse and dynamic group in programming languages and verification. Our group has active projects in areas such as static and dynamic program analysis; verification, debugging, and programmer productivity tools; language-based security; type systems; language design, compilation, and analysis for dynamic, web languages; performance analysis of data center-scale systems; analysis of hybrid and embedded systems. We have a track record of publishing in top venues, such as POPL and PLDI. CS Admissions (deadline December 15, 2011) and ECEE Admissions (deadline February 1, 2012 but earlier for financial aid consideration).

2011.09.09

Sam Blackshear is presenting the paper "The Flow-Insensitive Precision of Andersen's Analysis in Practice" at SAS 2011 on September 14.

2011.07.11

We will have a workshop with visitors Swarat Chaudhuri (Rice University, USA), Eric Goubault (CEA, France), Sylvie Putot (CEA, France), and César Sánchez (IMDEA, Spain) in ECOT 832 on July 12 10:00am-6:00pm.

2011.07.07

Eric Goubault and Sylvie Putot visit July 11-12.

2011.07.07

Swarat Chaudhuri visits July 11-15.

2011.07.01

César Sánchez visits July 5-August 12.

2011.06.02

Franjo Ivančić visits June 4.

2011.04.25

Christoph Reichenbach from U of Massachusetts, Amherst and alumnus of this group is visiting us on Monday, April 25, 2011. He is giving a talk at 10:00am in ECOT 832.

PLV Seminar

Christoph Reichenbach
University of Massachusetts, Amherst

04-25-2011 10:00
ECOT 832

What can the Garbage Collector compute efficiently? A Language for Heap Assertions at Garbage Collection Time

Abstract

Finding bugs is among the most challenging tasks in software development. For this reason, modern software development methodologies encourage programmers to use assertions throughout their code to express the assumptions they are making. At runtime, these assertions then detect whenever the assumptions do not match the program; in other words, they detect bugs early. However, traditional assertion mechanisms in mainstream languages such as C or Java are limited in their expressivity.

This talk presents DeAL, a rich heap assertion language for Java that extends over the expressive power of traditional assertions. DeAL introduces additional primitives to reason over heap layout, allowing programmers to assert global invariants, ownership, and other properties that would be impossible to express in traditional assertions.

By design, all DeAL assertions require only a single heap traversal and can execute as part of garbage collection. Consequently, DeAL is not only expressive, but also ensures a very low execution overhead.

2011.02.22

Aaron Stump from U of Iowa is visiting us February 24-25, 2011. He is giving a talk on Thursday, February 24 at 4:30pm in ECOT 832.

PLV Seminar

Aaron Stump
University of Iowa

02-24-2011 16:30
ECOT 832

Building Verified Software with Dependent Types

Abstract

Recent years have seen intensive interest among Programming Language (PL) researchers in connecting PL and Verification. Static analyses which once were primarily intended for enabling optimizations in compilers are now used also for program verification and bug finding. Type systems, which had been used to detect (either statically or dynamically) low-level bugs, are now pushed to express stronger and stronger semantic properties of code. Arguably the most powerful such systems known are so-called dependent type systems, which combine programming and theorem proving, and use rich types to express general logical specifications of programs.

In this talk, I will describe ongoing work in my group to design, prove, and implement dependently typed programming languages, and apply them for challenging case studies. I will summarize the design of the Guru dependently typed programming language, and explain how it overcomes some traditional difficulties for dependently typed languages, concerning general recursion and also the treatment of equality. For a case study, I will describe recent work of my doctoral student Duckki Oe to implement a statically verified modern SAT solver called versat in Guru. Versat uses the efficient low-level data structures and algorithms of modern solvers like Minisat, but has been statically verified to be sound: if versat reports "unsat", then the input formula is truly contradictory. Versat can solve benchmarks on the modern scale, including some from the SAT Competition 2009. I will conclude with a glimpse at a new dependently typed language called Trellys, being designed and implemented in a collaborative project with Stephanie Weirich at U. Pennsylvania and Tim Sheard at Portland State.

Biography

Aaron Stump is an associate professor of Computer Science at The University of Iowa, where he co-leads the U. Iowa Computational Logic Center with Cesare Tinelli. Aaron received his PhD in Computer Science in 2002 from Stanford University. His research interests are in Computational Logic and Programming Languages, with current focus on dependently typed programming languages and high-performance proof checking.

2011.02.06

Byron Cook from MSR Cambridge and Queen Mary, University of London is visiting us Tuesday, February 8, 2011. He is giving a talk at 3:00pm in ECOT 831.

PLV Seminar

Byron Cook
MSR Cambridge and Queen Mary, University of London

02-08-2011 15:00
ECOT 831

Proving stabilisation of biological models

Abstract

I will describe an efficient procedure for proving stabilisation of biological systems when modeled as qualitative networks or genetic regulatory networks. For scalability, we use modular proof techniques, where state-space exploration is applied only locally to small pieces of the system rather than the entire system as a whole. Our procedure exploits the observation that, in practice, the form of modular proofs can be restricted to a very limited set. Using our new procedure, we have solved a number of challenging published examples, including: a 3-D model of the mammalian epidermis; a model of metabolic networks operating in type-2 diabetes; a model of fate determination of vulval precursor cells in the C. elegans worm; and a model of pair-rule regulation during segmentation in the Drosophila embryo. Our results show many orders of magnitude speedup in cases where previous stabilization proving techniques were known to succeed, and new results in cases where tools had previously failed.

Biography

Dr. Byron Cook is a principal researcher at Microsoft Research Cambridge, as well as Professor of Computer Science at Queen Mary, University of London. Byron is one of the developers behind the Terminator program termination prover, as well as the SLAM symbolic software model checker which forms the basis of the Windows Static Driver Verifier tool.

2010.08.01

Chao Wang from NEC Laboratories and CU alumnus is visiting us August 26-27. He is giving a talk in the CS Colloquium on Thursday, August 26 3:30pm-4:30pm in ECCR 150.

PLV Seminar

Chao Wang
NEC Laboratories

08-26-2010 15:30
ECCR 150

Symbolic Predictive Analysis for Concurrent Programs

Abstract

Multi-core and multi-processor systems are becoming increasingly popular. However, our ability to effectively harness the power of parallelism is predicated upon advances in tools and algorithms for verifying concurrent programs. Concurrent programs are notoriously difficult to verify, and a key reason for this is the behavioral complexity resulting from the large number of interleavings of concurrent threads.

In this talk, I will introduce a symbolic predictive analysis for runtime detection of concurrency errors, by monitoring and subsequently analyzing the execution traces of a program. In this analysis, we first derive a symbolic predictive model using the trace information collected at run time as well as the program source code. What this model captures are not just the given traces, but all possible interleavings of events of these traces. Then we use symbolic reasoning to check whether there are concurrency errors in any of these interleavings. This is done by capturing these interleavings and the error conditions using a set of first-order logic formulas, and then deciding the formulas using an off-the-shelf Satisfiability Modulo Theory (SMT) solver.

Biography

2010.07.27

Xavier Rival from INRIA Roquencourt and ENS Paris is visiting us August 19-25. He is giving a talk on the Astrée Static Analyzer on Tuesday, August 24 at 11:00am in ECOT 831, and he is also giving a more in-depth demonstration of Astrée on Wednesday, August 25 4:00pm-5:00pm in ECST 1B21.

PLV Seminar

Xavier Rival
INRIA Roquencourt and ENS Paris

08-24-2010 11:00
ECOT 831

The Astrée Analyzer: Proving the absence of runtime errors automatically

Abstract

Runtime errors in embedded softwares may have disastrous consequences, e.g. in transportation or energy production systems.

The Astrée analyzer aims at proving the absence of runtime errors in C programs and was designed specifically for synchronous applications as found in fly-by-wire systems. The analysis process is conservative, that is, it may fail to establish the correctness of some safe programs, but it is sound, that is it will report any runtime error.

Astrée performs Abstract Interpretation based static analysis, that is abstract execution, using families of predicates formed by abstract domains. Astrée relies on a library of numerical and symbolic abstract domains, which allow to capture salient properties of embedded softwares, so as to establish absence of runtime errors. The analysis process is fully automatic, and involves automatic parameterization of the abstract domains.

We will present the underlying concepts of Astrée, and examplify the use of the analyzer on a few selected examples.

The Astrée analyzer has allowed to prove the absence of runtime errors in industrial size avionics programs. As of today, Absint Angewandte Informatik provides commercial diffusion and support of Astrée.

2010.07.27

Franjo Ivančić visits August 2.

2010.07.26

Byron Cook from MSR Cambridge and Queen Mary, University of London is visiting us Thursday, July 29, 2010. He is giving a talk in the CS Colloquium at 11:00am in ECOT 831.

PLV Seminar

Byron Cook
MSR Cambridge and Queen Mary, University of London

07-29-2010 11:00
ECOT 831

New methods for proving temporal properties of infinite-state systems

Abstract

I will describe some new methods of proving temporal properties of infinite-state programs. Our approach takes advantage of the fact that linear-temporal properties can often be proved more efficiently using proof techniques usually associated with the branching-time logic CTL. The caveat is that, in certain instances, nondeterminism in the system's transition relation can cause CTL methods to report counterexamples that are spurious in LTL. To address this problem we describe an algorithm that, as it attempts to apply CTL proof methods, finds and then removes problematic nondeterminism via an analysis on the spurious counterexamples. We must also develop CTL symbolic model checking tools for infinite-state systems.

Biography

Dr. Byron Cook is a Principal Researcher at Microsoft Research in Cambridge, UK as well as Professor of Computer Science at Queen Mary, University of London. He is one of the developers of the Terminator program termination proving tool, as well as the SLAM software model checker. Before joining Microsoft Research he was a developer in the WIndows OS kernel group. See research.microsoft.com/~bycook/ for more information.

2010.07.05

Siddharth Suryanarayanan from Colorado School of Mines is visiting us on Monday, July 19, 2010. He is giving a talk in the CS Colloquium at 3:00pm in DLC 1B70.

PLV Seminar

Siddharth Suryanarayanan
Colorado School of Mines

07-19-2010 15:00
DLC 1B70

Realizing the Smart Grid through smart interfaces, microgrids, and active distribution networks

Abstract

The electricity infrastructure in the US is poised to undergo unprecedented modernization aided by the "Smart Grid Initiative" for achieving high levels of reliability, efficiency, and interconnection of "green" resources. While the advantages of achieving the Smart Grid Initiative appear bountiful, there are concomitant challenges to realizing this transformation. This talk will describe the present state and future trends of the electricity infrastructure, and the need for Smart Grid legislation. The crux of the seminar will focus on how to realize the Smart Grid Initiative's full impact by innovative research and development on:

  • Smart interfaces between renewable sources and the electricity grid,
  • Energy efficient electric power microgrids, and
  • Transformation from a passive to active electric distribution network.

Biography

Sid Suryanarayanan is from Chennai, India. He received the Ph.D. in electrical engineering from Arizona State University (ASU) in May 2004. Since January 2008 he has held an Assistant Professor position in the Division of Engineering at Colorado School of Mines (CSM) in Golden, CO. From fall 2010, he will begin an Assistant Professorship in the Dept. of Electrical and Computer Engineering (ECE) at Colorado State University. Prior to that he held research appointments in the faculties of Florida State University and ASU. Sid currently performs sponsored research in the areas of electric power microgrids and the impact of the Smart Grid Initiative on electric power systems.

2010.03.15

Benjamin C. Pierce from UPenn is visiting Thursday, April 29, 2010. He is giving a talk in the CS Colloquium at 3:30pm in ECCR 265.

PLV Seminar

Benjamin C. Pierce
University of Pennsylvania

04-29-2010 15:30
ECCR 265

How to Build Your Own Bidirectional Programming Language

Abstract

Most programs get used in just one direction, from input to output. But sometimes, having computed an output, we need to be able to update this output and then "calculate backwards" to find a correspondingly updated input. The problem of writing such bidirectional transformations -- often called lenses -- arises in applications across a multitude of domains and has been attacked from many perspectives. Potential applications include synchronization of replicated data, system configuration management tools (such as RedHat's Augeas system), bidirectional transformations between software models, and updatable "security views."

The Harmony project at the University of Pennsylvania is exploring a linguistic approach to bidirectional programming, designing domain-specific languages in which every expression simultaneously describes both parts of a lens. When read from left to right, an expression denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an "update translator" that takes an input together with an updated output and produces a new input that reflects the update. These languages share some common elements with modern functional languages -- in particular, they come with very expressive type systems. In other respects, they are rather novel and surprising.

We have designed, implemented, and applied bi-directional languages in three quite different domains: a language for bidirectional transformations on trees (such as XML documents), based on a collection of primitive bidirectional tree transformation operations and "bidirectionality-preserving" combining forms; a language for bidirectional views of relational data, using bidirectionalized versions of the operators of relational algebra as primitives; and, most recently, a language for bidirectional string transformations, with primitives based on standard notations for finite-state transduction and a type system based on regular expressions. The string case is especially interesting, both in its own right and because it exposes a number of foundational issues common to all bidirectional programming languages in a simple and familiar setting. We are also exploring how lenses and their types can be enriched to embody privacy and integrity policies.

This talk explores the design of bidirectional languages, starting from the very simplest imaginable variant (bijective languages) and then developing several refinements.

Biography

Benjamin Pierce joined the CIS Department at Penn in 1998. Previously, he was on the faculty at Indiana University and held research fellowships at Cambridge University, the University of Edinburgh, and INRIA-Roquencourt. He received his PhD in Computer Science at Carnegie Mellon University in 1991. His research centers on programming languages, static type systems, concurrent and distributed programming, and synchronization technologies. His books include the widely used graduate text Types and Programming Languages. He is also the lead designer of the popular Unison file synchronizer.

2010.03.12

Martin Burtscher from UT Austin and CU alumnus is visiting Thursday, March 18, 2010. He is giving a talk in the CS Colloquium at 3:30pm in ECCR 265.

PLV Seminar

Martin Burtscher
The University of Texax at Austin

03-18-2010 15:30
ECCR 265

Towards a Science of Parallel Programming

Abstract

When parallel programming started in the 70s and 80s, it was mostly art: languages such as functional and logic programming languages were designed and appreciated mainly for their elegance and beauty. More recently, parallel programming has become engineering: conventional languages like FORTRAN and C++ have been extended with constructs such as OpenMP, and we now spend our time benchmarking and tweaking large programs nobody understands to obtain performance improvements of 5-10%. In spite of all this activity, we have few insights into how to write parallel programs to exploit the performance potential of multicore processors.

To break this impasse, we need a science of parallel programming. In this talk, I will introduce a concept called "amorphous data-parallelism" that provides a simple, unified picture of parallelism in a host of diverse applications ranging from mesh generation/refinement/partitioning to SAT solvers, maxflow algorithms, stencil computations, and event-driven simulation. Then I will present a natural classification that provides insight into the structure of parallelism and locality in these algorithms and into appropriate language and systems support for exploiting this parallelism.

Biography

Martin Burtscher received the combined BS/MS degree in computer science from the Swiss Federal Institute of Technology (ETH) Zurich in 1996 and the PhD degree in computer science from the University of Colorado Boulder in 2000. Since then, he has been an assistant professor in the School of Electrical and Computer Engineering at Cornell University and a Research Scientist in the Institute for Computational Engineering and Sciences at the University of Texas at Austin. His current research focuses on automatic parallelization of irregular programs for multicore and GPU architectures as well as on automatic performance assessment and optimization of HPC applications. He is an associate editor of the Journal of Instruction-Level Parallelism and a senior member of the IEEE, its Computer Society, and the ACM.

2010.02.22

Brad Chen from Google is visiting us Thursday, February 25, 2010. He is giving a talk in the CS Colloquium at 3:30pm in ECCR 265.

PLV Seminar

Brad Chen
Google

02-25-2010 15:30
ECCR 265

The Desktop: Frontiers in Systems Research

Hosted by .

Abstract

Desktop software, in the form of web browsers, browser features, and OS distributions, are a growing area of engineering activity at Google. This talk will give an overview of this work, looking in detail at Native Client as an example project in the space. Native Client is an open-source research technology for running x86 native code in web applications, with the goal of maintaining the browser neutrality, OS portability, and safety that people expect from web apps. It supports performance-oriented features generally absent from web application programming environments, such as thread support, instruction set extensions such as SSE, and use of compiler intrinsics and hand-coded assembler. We combine these properties in an open architecture designed to leverage existing web standards, and to encourage community review and third-party tools. Overall, Google's desktop efforts seek to enable new Web applications, improve end-user experience, and enable a more flexible balance between client and server computing. Google has open sourced many of our desktop efforts, in part to encourage collaboration and independent innovation.

Biography

J. Bradley Chen manages the Native Client project at Google, where he has also worked on cluster performance analysis projects. Prior to joining Google, he was Director of the Performance Tools Lab in Intel's Software Products Division. Chen served on the faculty of Harvard University from 1994-1998, conducting research in operating systems, computer architecture and distributed system, and teaching a variety of related graduate and undergraduate courses. He has published widely on the subjects of systems performance and computer architecture. Dr. Chen has bachelors and masters degrees from Stanford University and a PhD from Carnegie Mellon University.

2010.01.13

Michelle Mills Strout from Colorado State is visiting us Thursday, January 28, 2010. She is giving a talk in the CS Colloquium at 3:30pm in ECCR 265.

PLV Seminar

Michelle Mills Strout
Colorado State University

01-28-2010 15:30
ECCR 265

Introducing the Sparse Polyhedral Framework

Abstract

Loops often dominate the execution time of applications. Various transformation frameworks have been developed to enable the automatic compile-time transformation of loops. Many of the existing models fit within the polyhedral framework and although they are quite powerful, they are restricted to compile-time transformations and loop bounds and memory accesses that are affine or can be approximated as affine.

In this talk, I will present the Sparse Polyhedral Framework (SPF). The SPF builds on the polyhedral programming model, but is also capable of expressing and supporting the code generation for run-time reordering transformations implemented with inspector/executor strategies. I will then discuss the idea of abstractions for exposing transformation frameworks in performance programmer models.

Biography

Michelle Mills Strout is an assistant professor of computer science at Colorado State University. She obtained her PhD in Computer Science from the University of California, San Diego in June 2003. In 2008, Michelle received a CAREER Award from the National Science Foundation for her research in parallelization techniques for irregular applications, such as molecular dynamics simulations. Her main research area is high performance computing and her research interests include compilers and run-time systems, scientific computing, and software engineering.

2010.01.06

Rastislav Bodik from UC Berkeley is visiting us Tuesday, January 11, 2010. He is giving a talk at 3:00pm in DLC 1B70.

PLV Seminar

Rastislav Bodik
University of California Berkeley

01-11-2010 15:00
DLC 1B70

Algorithmic Program Synthesis with Partial Programs

Abstract

Why hasn't Moore's Law revolutionize programming? In model checking, cycles fuel bug discovery, improving code quality, but programmers still write programs with their bare hands. In fact, their work has not changed much since the CRT terminal, except that they think in better languages.

Program synthesis might be a way to reduce the programmer's cognitive load. Synthesizers have derived programs that were highly efficient, and sometimes even surprising. Of course, they had to be first "programmed" with the human insights about the domain at hand.

Which brings us to a key problem in program synthesis --- how to communicate human expertise to the synthesizer. In deductive synthesis, this expertise is captured in a domain theory. Often elusive even to formally trained experts, a domain theory is probably not a shortcut to programmer productivity.

This talk will describe a growing family of synthesizers based on partial programs. Their premise is that programs can be decomposed into insight and mechanics: if the programmer encodes her insight as a partial program, the mechanics can then be synthesized given a specification. Partial programs lend themselves to algorithmic synthesis: rather than deducing a program with a theorem prover, algorithmic synthesis finds the program in a space of candidate implementations described by the partial program.

Among five synthesizers, I will describe an algorithm for finding a candidate by constraint solving, rather than via generate-and-test, and a system for programming with angelic non-determinism which computes the insight into a programming problem.

Biography

Ras Bodik is an Associate Professor of Computer Science at UC Berkeley. He is interested in programming systems, from static and dynamic analysis to programmer tools. He leads a project of program synthesis for high-performance programs based on the idea of program sketches. He also leads a project on parallel web browsers for mobile devices, which develops parallel parsing and page layout algorithms, as well as a constraints-based scripting language.

2009.06.05

Lars Birkedal visits July 3.

2009.03.04

Frank Pfenning visits March 6.