BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//TYPO3/NONSGML News system (news)//EN
BEGIN:VEVENT
UID:news-25743@cs.au.dk
DTSTAMP:20260326T095612Z
DTSTART:20260409T080000Z
DTEND:20260409T090000Z
END:VEVENT
END:VCALENDAR




<div class="news news-single">
	<div class="article" itemscope="itemscope" itemtype="http://schema.org/Article">
		
	
			<script type="text/javascript">
				const showAllContentLangToken = "Show all content ";
			</script>

			
			

			<article class="typo3-delphinus delphinus-gutters">

				<!-- News PID: 4980 - used for finding folder/page which contains the news / event -->
				<!-- News UID: 25743 - the ID of the current news / event-->

				<div class="news-event">
					<div class="news-event__header">
						<!-- Categories -->
						
							<span class="text--stamp">
<!-- categories -->
<span class="news-list-category">
	
		
	
</span>

</span>
						

						<!-- Title -->
						<h1 itemprop="headline">Special talk by Alejando Aguirre on High-assurance verification for real-world probabilistic programs</h1>
						
					</div>

					
						<!-- Top image -->
						
					

					<div class="news-event__content">

						<!-- Events info box -->
						
								

								<div class="news-event__info theme--dark" id="event-info">
									<h2 class="screenreader-only">Info about event</h2>

									
											<!--- Same date -->
											<div class="news-event__info__item news-event__info__item--time">
												<h3 class="news-event__info__item__header text--label-header">Time</h3>
												<div class="news-event__info__item__content">
													<span class="u-avoid-wrap">
														Thursday  9  April 2026,
													</span>
													<span class="u-avoid-wrap">
														&nbsp;at 10:00 -  11:00
													</span>
													<p class="news-event__info__item__ical-link"><a href="/news-events/events/show-event/artikel/default-c222e58b3cc9a1b17c6bbae32675f435?tx_news_pi1%5Bformat%5D=ical&amp;type=9819&amp;cHash=9df8364f442beb513bc741038a1bfb98">Add to calendar</a></p>
												</div>
											</div>
										

									<!-- Location detailed -->
									
											<!-- Location Simple -->
											
												<div class="news-event__info__item">
													<h3 class="news-event__info__item__header text--label-header">Location</h3>
													<div class="news-event__info__item__content">
														<p>Ada-333</p>
													</div>
												</div>
											
										

									<!-- Organizer detailed -->
									
											<div class="news-event__info__item">
												<h3 class="news-event__info__item__header text--label-header">Organizer</h3>
												<div class="news-event__info__item__content">
													Department of Computer Science, Aarhus University
												</div>
												
													<div class="news-event__info__item__link">
														<a href="/">Åbogade 34, 8200 Aarhus N, Denmark.</a>
													</div>
												
											</div>
										

									<!-- Price -->
									

									<!-- Event link -->
									

									<!-- Registration -->
									
								</div>
							

						
							<!-- Media -->
							
								



							
						

						
							<div class="news-event__content__text">
								<span class="text--byline" id="byline">
									

									<!-- Author -->
									
										<span itemprop="author" itemscope="itemscope" itemtype="http://schema.org/Person">
											
													By
												

											
													<a href="mailto:skm@cs.au.dk">
														<span itemprop="name">Søs Küster Markussen</span>
													</a>
												
										</span>
									
								</span>

								

									<!-- Body text -->
									<p>Abstract:</p>
<p>Probabilistic programs, that is, programs that use randomness in their execution, appear everywhere in modern computing. For example, in randomized algorithms, where randomization is used to increase efficiency, or in cryptography, where it is used to ensure security. Although the principles that make these algorithms and protocols work are generally well-understood, these programs are ultimately written in industrial languages, and the interaction between randomization and the rest of the language features makes these critical programs hard to reason about. In this talk, I will present my work, which focuses on developing formal methods and tools to reason about probabilistic programs written in realistic programming languages. These techniques have been implemented in the proof assistant Rocq, which both gives us strong correctness guarantees, and also allows us to scale them up beyond the scope of previous work.</p>
								
							</div>
						
					</div>

					
						<!-- Content elements -->
						
					
				</div>
			</article>

			
				
				
			

			<!-- related things -->
			
		

	</div>
</div>