https://m2.mtmt.hu/ hun 2026-09-21 03:48 JournalArticle 33784283 VALIDATED true Conference code: 199105 Export Date: 10 May 2024 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding text 1: Funding. This research was partially funded by the \\u00DANKP-22-{2,3}-I New National Excellence Program and the 2019-1.3.1-KK-2019-00004 project from the National Research, Development and Innovation Fund of Hungary. WoS:hiba:001313392600008 2025-03-21 06:13 DOI azonosító nem egyezik 0 false 2026-09-01T13:25:58.532+0000 2025-04-03T12:26:52.974+0000 2023-04-30T15:37:43.224+0000 true 10073070 Bajczi Levente /api/author/10073070 Author Bajczi Levente (informatika) true 2025-04-03T12:24:18.770+0000 2025-04-03T12:24:18.770+0000 2025-04-03T12:26:50.203+0000 true 10051300 Háromszéki-Virág Fruzsina /api/admin/10051300 Admin Háromszéki-Virág Fruzsina (MTMT Központi admin) true 10051300 2025-04-03T12:26:53.116+0000 true 10051300 Háromszéki-Virág Fruzsina /api/admin/10051300 Admin Háromszéki-Virág Fruzsina (MTMT Központi admin) true 10051300 true false true 24 24 /api/publicationtype/24 PublicationType Folyóiratcikk 1 true 24 JournalArticle true 1268360 Conference paper in journal true 24 24 /api/publicationtype/24 PublicationType Folyóiratcikk 1 true 24 JournalArticle /api/subtype/1268360 Konferenciaközlemény SubType Konferenciaközlemény (Folyóiratcikk) 109 true 1268360 true 1 /api/category/1 Category Tudományos true 1 Somorjai, Márk true false /api/journal/10060597 REVIEWED ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE 2075-2180 true false 10060597 true 10060597 false 2075-2180 Journal FOREIGN 402 402 105 117 105 13 2024 true 339518 /api/conference/339518 true 14471 true 10020 /api/country/10020 Country Olaszország true 16 /api/city/14471 City Rome, Olaszország true 10005563 Conference 18th Logical and Semantic Frameworks with Applications, LSFA 2023 2023-07-01 [Rome, Olaszország] true Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. © Márk Somorjai et al. true 2023 true true true true true false GOLD 2026-09-01 false https://cgi.cse.unsw.edu.au/~eptcs/ 6 0 6 6 0 6 6 4 5 6 6 6 6 6 0 0 6 6 6 6 0 2 2 Folyóiratcikk Journal Article 24 2 Könyvrészlet Chapter in Book 25 4 Könyv Book 23 0 Egyéb konferenciaközlemény Conference paper 31 0 Egyéb konferenciakötet Conference proceedings 32 0 Oltalmi formák Protection forms 26 0 Disszertáció Thesis 28 0 Egyéb Miscellaneous 29 0 Alkotás Achievement 22 0 Kutatási adat Research data 33 0 Folyóiratcikk Journal Article 24 0 0 0 Könyvrészlet Chapter in Book 25 0 0 0 Könyv Book 23 0 0 0 Egyéb konferenciaközlemény Conference paper 31 0 0 0 Egyéb konferenciakötet Conference proceedings 32 0 0 0 Oltalmi formák Protection forms 26 0 0 0 Disszertáció Thesis 28 0 0 0 Egyéb Miscellaneous 29 0 0 0 Alkotás Achievement 22 0 0 0 Kutatási adat Research data 33 0 0 0 2025 0 5 5 5 5 2026 0 1 1 1 1 false 10042280 false false false 2023-07-29T15:38:17.435+0000 Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Méréstechnika és Információs Rendszerek Tanszék (BME / VIK) 5 17 2 5 0 false Language 10002 /api/language/10002 Angol Angol English true 2 true PersonAuthorship 107531326 /api/authorship/107531326 Somorjai, Márk [Somorjai, Márk (Informatika), szerző] Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT) 1 0.2 true false Author 10088738 /api/author/10088738 Somorjai Márk (Informatika) Somorjai Márk true true Somorjai Márk true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 107531327 /api/authorship/107531327 Dobos-Kovács, Mihály [Dobos-Kovács, Mihály (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT) 2 0.2 false false Author 10073065 /api/author/10073065 Dobos-Kovács Mihály (informatika) Dobos-Kovács Mihály true true Dobos-Kovács Mihály true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 107531329 /api/authorship/107531329 Ádám, Zsófia [Ádám, Zsófia (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK) 3 0.2 false false Author 10077295 /api/author/10077295 Ádám Zsófia (informatika) Ádám Zsófia true true Ádám Zsófia true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 107531328 /api/authorship/107531328 Bajczi, Levente [Bajczi, Levente (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT) 4 0.2 false false Author 10073070 /api/author/10073070 Bajczi Levente (informatika) Bajczi Levente true true Bajczi Levente true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PersonAuthorship 107531330 /api/authorship/107531330 Vörös, András [Vörös, András (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT) 5 0.2 false true Author 10042280 /api/author/10042280 Vörös András (informatika) Vörös András true 10042280 true Vörös András true false false AuthorshipType 1 /api/authorshiptype/1 Szerző 0 true 0 true false true PublicationIdentifier 26083872 /api/publicationidentifier/26083872 DOI: 10.4204/EPTCS.402.11 PlainSource 6 /api/publicationsource/6 DOI PublicationSourceType 10001 /api/publicationsourcetype/10001 DOI true true true DOI DOI https://doi.org/@@@ true true 6 true IDENTICAL 10.4204/EPTCS.402.11 https://doi.org/10.4204/EPTCS.402.11 false true PublicationIdentifier 27561005 /api/publicationidentifier/27561005 WoS: 001313392600008 PlainSource 1 /api/publicationsource/1 WoS PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true WoS WoS https://www.webofscience.com/wos/woscc/full-record/@@@ true true 1 true IDENTICAL 001313392600008 https://www.webofscience.com/wos/woscc/full-record/001313392600008 false true PublicationIdentifier 26161724 /api/publicationidentifier/26161724 Scopus: 85191659480 PlainSource 3 /api/publicationsource/3 Scopus PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true Scopus Scopus http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-@@@ true true 3 true IDENTICAL 85191659480 http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85191659480 false true PublicationIdentifier 26083873 /api/publicationidentifier/26083873 Egyéb URL: https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LSFA2023.11 PlainSource 40 /api/publicationsource/40 Egyéb URL PublicationSourceType 10006 /api/publicationsourcetype/10006 Link true true true Egyéb URL Other URL @@@ true true 40 true IDENTICAL https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LSFA2023.11 https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LSFA2023.11 false true Classification 10034 /api/classification/10034 Számítás- és információtudomány true true /api/publication/33784283 Somorjai Márk et al. Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification. (2024) ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE 2075-2180 402 402 105-117<div class="JournalArticle Publication long-list"> <div class="authors"> <img title="Forrásközlemény" style="float: left" src="/frontend/resources/grid/publication-core-icon.png"> <img title="Idézőközlemény" style="float: left" src="/frontend/resources/grid/publication-citation-icon.png"> <div class="autype autype0"> <span class="author-name" mtid="10088738"><a href="/gui2/?type=authors&mode=browse&sel=10088738" target="_blank">Somorjai Márk (<span class="authorship-author-name">Somorjai Márk</span> <span class="authorAux-mtmt"> Informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/<span title="Mesterséges Intelligencia és Rendszertervezés Tanszék">MIT</span>/Kritikus Rendszerek Kutatócsoport</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10073065"><a href="/gui2/?type=authors&mode=browse&sel=10073065" target="_blank">Dobos-Kovács Mihály (<span class="authorship-author-name">Dobos-Kovács Mihály</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Méréstechnika és Információs Rendszerek Tanszék; <span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/<span title="Mesterséges Intelligencia és Rendszertervezés Tanszék">MIT</span>/Kritikus Rendszerek Kutatócsoport</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10077295"><a href="/gui2/?type=authors&mode=browse&sel=10077295" target="_blank">Ádám Zsófia (<span class="authorship-author-name">Ádám Zsófia</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Méréstechnika és Információs Rendszerek Tanszék</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10073070"><a href="/gui2/?type=authors&mode=browse&sel=10073070" target="_blank">Bajczi Levente (<span class="authorship-author-name">Bajczi Levente</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Méréstechnika és Információs Rendszerek Tanszék; <span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/<span title="Mesterséges Intelligencia és Rendszertervezés Tanszék">MIT</span>/Kritikus Rendszerek Kutatócsoport</span> ;&nbsp;&nbsp;&nbsp; <span class="author-name" mtid="10042280"><a href="/gui2/?type=authors&mode=browse&sel=10042280" target="_blank">Vörös András (<span class="authorship-author-name">Vörös András</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/Méréstechnika és Információs Rendszerek Tanszék; <span title="Budapesti Műszaki és Gazdaságtudományi Egyetem">BME</span>/<span title="Villamosmérnöki és Informatikai Kar">VIK</span>/<span title="Mesterséges Intelligencia és Rendszertervezés Tanszék">MIT</span>/Kritikus Rendszerek Kutatócsoport</span> </div> </div> <div class="title"><a href="/gui2/?mode=browse&params=publication;33784283" target="_blank">Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification</a></div> <div> <span class="journal-title">ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE</span> <span class="journal-issn">( <a target="_blank" href="https://portal.issn.org/resource/ISSN/2075-2180">2075-2180</a>)</span>: <span class="journal-volume">402</span> <span class="journal-issue">402</span> <span class="page"> pp 105-117 </span> <span class="year">(2024)</span> <div class="conference"> 18th Logical and Semantic Frameworks with Applications, LSFA 2023. Konferencia helye, ideje: <span class="location">Rome, Olaszország <span class="conference-date">2023.07.01. - 2023.07.02.</span> </div> </div> <div class="pub-footer"> <span class="language" xmlns="http://www.w3.org/1999/html">Nyelv: Angol | </span> <span class="identifiers"> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="10.4204/EPTCS.402.11" target="_blank" href="https://doi.org/10.4204/EPTCS.402.11"> DOI </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="001313392600008" target="_blank" href="https://www.webofscience.com/wos/woscc/full-record/001313392600008"> WoS </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="85191659480" target="_blank" href="http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85191659480"> Scopus </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LSFA2023.11" target="_blank" href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LSFA2023.11"> Egyéb URL </a> </span> </span> <div class="publication-citation" style="margin-left: 0.5cm;"> <span title="Nyilvános idézőközlemények összesen, említések nélkül" class="citingPub-count">Nyilvános idéző összesen: 6</span> | Független: 6 | Függő: 0 | Nem jelölt: 0 | WoS jelölt: 4 | Scopus jelölt:&nbsp;5 | WoS/Scopus jelölt:&nbsp;6 | DOI jelölt:&nbsp;6 </div> <div class="publication-citation"> <a target="_blank" href="/api/publication?cond=citations.related;eq;33784283&sort=publishedYear,desc&sort=title"> Idézett közlemények száma: 2 </a> </div> <div class="mtid"><span class="long-pub-mtid">Közlemény: 33784283</span> | <span class="status-data status-VALIDATED"> Egyeztetett </span> Forrás Idéző | <span class="type-subtype">Folyóiratcikk ( Konferenciaközlemény ) </span> | <span class="pub-category">Tudományos</span> | <span class="publication-sourceOfData">kézi felvitel</span> </div> <div class="lastModified">Utolsó módosítás: 2025.04.03. 14:26 Háromszéki-Virág Fruzsina (MTMT Központi admin) </div> <pre class="comment" style="margin-top: 0; margin-bottom: 0;"><u>Megjegyzés</u>: Conference code: 199105 Export Date: 10 May 2024 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding text 1: Funding. This research was partially funded by the \\u00DANKP-22-{2,3}-I New National Excellence Program and the 2019-1.3.1-KK-2019-00004 project from the National Research, Development a...</pre> </div></div>