Programming Languages and Verification at the University of Colorado Boulder

Boulder, Colorado, USA
Colorado PLV retweeted
📢📢CU Boulder is hiring TT faculty in Trustworthy & Scalable AI Systems. We would love to see applications from PL/FM/SE folks! jobs.colorado.edu/jobs/JobDe…
4
5
1,085
Colorado PLV retweeted
We're excited to have @neharungta as a keynote speaker and can't wait to see you in Pasadena! More keynote details here: 2024.splashcon.org/track/spl…
In a #SPLASH keynote, I talk about our work on formally verifying the authorization engine in AWS, which handles trillions of daily requests. Witness formal methods at cloud scale in Pasadena, CA. Join us: 2024.splashcon.org/track/spl…
4
11
2,985
Colorado PLV retweeted
Another fantastic day @cuplv this week, this time hosting @suresh12345!
1
1
13
895
Colorado PLV retweeted
We had a fantastic day hosting @ShriramKMurthi and learning about the human factors of formal methods!!
1
18
905
Several PhD positions in CUPLV, the Programming Languages and Verification Group (plv.colorado.edu), and the CS Department at CU Boulder!
2
4
3
2,533
Join CU CS for the virtual session on December 13 to gain a deeper understanding of PhD requirements, application submission, and the admissions process! You can access the sessions here: shorturl.at/rsMR0.
113
PhD opportunities with CUPLV are centered around the formal study of computational systems ranging across interactive, mobile, distributed, cyber-physical, and autonomous, with a focus on leveraging techniques from programming languages, control theory, and machine learning.
86
Colorado PLV retweeted
CUPLV at @splashcon Portugal 😎
2
11
533
Colorado PLV retweeted
Replying to @KirbyLinvill
@KirbyLinvill’s @splashcon talk on Verifying Privacy-Preserving Protocols is today! If you are around, drop by Room 12 at 15:12 and check out Kirby’s cool work on probabilistic reasoning about distributed programs!
Replying to @cuplv
2. @KirbyLinvill and co-authors @GowthamK and @ewust show how Dependent Types + Lipton's movers ⟹ automatic verification of probabilistic privacy properties. The tool Waldo found potential privacy violations in the TLS ECH spec and helpe verify the fixed implementation in F*.
1
4
174
Also, watch for @bechang's keynote at this year's SAS (co-located with OOPSLA) along with his paper (with Amazon co-authors) on Lifting On-Demand Analysis to Higher-Order Languages.
4
113
📣Two CUPLV papers at OOPSLA this year! 1. @MeierShawn and co-authors Sergio Mover, @GowthamK, and @bechang demonstrate how to do scalable reachability analysis in presence of callbacks. The tool Historia has analyzed 2M lines of android app source code and found real bugs!
1
3
19
1,244
2. @KirbyLinvill and co-authors @GowthamK and @ewust show how Dependent Types + Lipton's movers ⟹ automatic verification of probabilistic privacy properties. The tool Waldo found potential privacy violations in the TLS ECH spec and helpe verify the fixed implementation in F*.
5
297
Colorado PLV retweeted
Niloofar is presenting our work on safety synthesis for partially observable systems using data @IFAC2023
2
11
1,254
Colorado PLV retweeted
Mahathi is presenting our paper on neural network based barrier certificate at @IFAC2023
1
10
804
Colorado PLV retweeted
Evan Chang on Interactive Abs Int #dagstuhl
1
2
5
418
Colorado PLV retweeted
Excited to receive the NSF Career award entitled “A Data-Driven Approach for Verification and Control of Cyber-Physical Systems”! shorturl.at/kJNRW
5
3
47
Sometimes “published” actually means published! @bechang 😎#pldi2022
1
2
45