<?xml version="1.0" encoding="UTF-8"?>

<modsCollection xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.loc.gov/mods/v3" xsi:schemaLocation="http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-3.xsd">
<mods version="3.3">

<genre>conference paper</genre>

<titleInfo><title>Refuting equivalence in probabilistic programs with conditioning</title></titleInfo>

  
  
<titleInfo type="alternative">
  
  <title>LNCS</title>
</titleInfo>

<note type="publicationStatus">published</note>


<note type="qualityControlled">yes</note>

<name type="personal">
  <namePart type="given">Krishnendu</namePart>
  <namePart type="family">Chatterjee</namePart>
  <role><roleTerm type="text">author</roleTerm> </role><identifier type="local">2E5DCA20-F248-11E8-B48F-1D18A9856A87</identifier><description xsi:type="identifierDefinition" type="orcid">0000-0002-4561-241X</description></name>
<name type="personal">
  <namePart type="given">Ehsan</namePart>
  <namePart type="family">Kafshdar Goharshadi</namePart>
  <role><roleTerm type="text">author</roleTerm> </role><identifier type="local">103b4fa0-896a-11ed-bdf8-87b697bef40d</identifier><description xsi:type="identifierDefinition" type="orcid">0000-0002-8595-0587</description></name>
<name type="personal">
  <namePart type="given">Petr</namePart>
  <namePart type="family">Novotný</namePart>
  <role><roleTerm type="text">author</roleTerm> </role><identifier type="local">3CC3B868-F248-11E8-B48F-1D18A9856A87</identifier></name>
<name type="personal">
  <namePart type="given">Dorde</namePart>
  <namePart type="family">Zikelic</namePart>
  <role><roleTerm type="text">author</roleTerm> </role><identifier type="local">294AA7A6-F248-11E8-B48F-1D18A9856A87</identifier><description xsi:type="identifierDefinition" type="orcid">0000-0002-4681-1699</description></name>







<name type="corporate">
  <namePart></namePart>
  <identifier type="local">KrCh</identifier>
  <role>
    <roleTerm type="text">department</roleTerm>
  </role>
</name>



<name type="conference">
  <namePart>TACAS: Tools and Algorithms for the Construction and Analysis of Systems</namePart>
</name>



<name type="corporate">
  <namePart>Formal Methods for Stochastic Models: Algorithms and Applications</namePart>
  <role><roleTerm type="text">project</roleTerm></role>
</name>



<abstract lang="eng">We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.</abstract>

<relatedItem type="constituent">
  <location>
    <url displayLabel="2025_TACAS_Chatterjee_Goharshadi.pdf">https://research-explorer.ista.ac.at/download/19744/19773/2025_TACAS_Chatterjee_Goharshadi.pdf</url>
  </location>
  <physicalDescription><internetMediaType>application/pdf</internetMediaType></physicalDescription><accessCondition type="restrictionOnAccess">no</accessCondition>
</relatedItem>
<originInfo><publisher>Springer Nature</publisher><dateIssued encoding="w3cdtf">2025</dateIssued><place><placeTerm type="text">Hamilton, ON, Canada</placeTerm></place>
</originInfo>
<language><languageTerm authority="iso639-2b" type="code">eng</languageTerm>
</language>



<relatedItem type="host"><titleInfo><title>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</title></titleInfo>
  <identifier type="issn">0302-9743</identifier>
  <identifier type="eIssn">1611-3349</identifier>
  <identifier type="isbn">9783031906527</identifier>
  <identifier type="arXiv">2501.06579</identifier><identifier type="doi">10.1007/978-3-031-90653-4_14</identifier>
<part><detail type="volume"><number>15697</number></detail><extent unit="pages">279-300</extent>
</part>
</relatedItem>


<extension>
<bibliographicCitation>
<short>K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 279–300.</short>
<apa>Chatterjee, K., Goharshady, E., Novotný, P., &amp;#38; Zikelic, D. (2025). Refuting equivalence in probabilistic programs with conditioning. In &lt;i&gt;31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems&lt;/i&gt; (Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. &lt;a href=&quot;https://doi.org/10.1007/978-3-031-90653-4_14&quot;&gt;https://doi.org/10.1007/978-3-031-90653-4_14&lt;/a&gt;</apa>
<chicago>Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Refuting Equivalence in Probabilistic Programs with Conditioning.” In &lt;i&gt;31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems&lt;/i&gt;, 15697:279–300. Springer Nature, 2025. &lt;a href=&quot;https://doi.org/10.1007/978-3-031-90653-4_14&quot;&gt;https://doi.org/10.1007/978-3-031-90653-4_14&lt;/a&gt;.</chicago>
<ieee>K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in &lt;i&gt;31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems&lt;/i&gt;, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.</ieee>
<ista>Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence in probabilistic programs with conditioning. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15697, 279–300.</ista>
<mla>Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” &lt;i&gt;31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems&lt;/i&gt;, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:&lt;a href=&quot;https://doi.org/10.1007/978-3-031-90653-4_14&quot;&gt;10.1007/978-3-031-90653-4_14&lt;/a&gt;.</mla>
<ama>Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in probabilistic programs with conditioning. In: &lt;i&gt;31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems&lt;/i&gt;. Vol 15697. Springer Nature; 2025:279-300. doi:&lt;a href=&quot;https://doi.org/10.1007/978-3-031-90653-4_14&quot;&gt;10.1007/978-3-031-90653-4_14&lt;/a&gt;</ama>
</bibliographicCitation>
</extension>
<recordInfo><recordIdentifier>19744</recordIdentifier><recordCreationDate encoding="w3cdtf">2025-05-25T22:17:10Z</recordCreationDate><recordChangeDate encoding="w3cdtf">2025-06-02T11:16:13Z</recordChangeDate>
</recordInfo>
</mods>
</modsCollection>
