DOI,IST REx ID,Research Group,Title of publication
10.1145/3729249,19936,MiSa,RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers
10.1145/3704847,21052,,"Program logics à la Carte"
10.1145/3704856,21053,,Formal foundations for translational separation logic verifiers
10.1145/3656422,17495,,RefinedRust: A type system for high-assurance verification of rust programs
10.1145/3656413,17497,,Quiver: Guided abductive inference of separation logic specifications in coq
10.1145/3622823,17498,,Melocoton: A program logic for verified interoperability between OCaml and C
10.1145/3571232,17499,,Conditional contextual refinement
10.1145/3571220,17500,,DimSum: A decentralized approach to multi-language semantics and verification
10.1145/3563345,17501,,BFF: Foundational and automated verification of bitfield-manipulating programs
10.1145/3498681,17503,,VIP: Verifying real-world C idioms with integer-pointer casts
10.1145/3498689,17504,,Simuliris: A separation logic framework for verifying concurrent program optimizations
10.1145/3371100,17506,,The high-level benefits of low-level sandboxing
10.1145/3290366,6380,KrCh,Efficient parameterized algorithms for data packing