International Center for Computational Logic - Benutzerbeiträge [de]

SEMECO-Q1

2025-03-19T09:15:09Z

Calvin Chau:

{{Projekt
|Kurzname=SEMECO-Q1
|Name=Sichere Medizinische Mikrosysteme und Kommunikation: Sichere & Vertrauenswürdige Systemarchitekturen
|Name EN=Secure Medical Microsystems and Communications: Secure & Trustworthy System Architecture
|Beschreibung DE=Weitere informationen finden Sie auf der [https://digitalhealth.tu-dresden.de/projects/semeco/ externen Projektwebseite].
|Beschreibung EN=For more information, see the [https://digitalhealth.tu-dresden.de/projects/semeco/ external project website].
|Kontaktperson=Christel Baier
|URL=https://digitalhealth.tu-dresden.de/projects/semeco/
|Start=01.05.2023
|Ende=30.04.2026
|Finanziert von=BMBF
|Projektstatus=aktiv
|Logo=Semeco-logo.png
|Person=Christel Baier, Calvin Chau
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings525714163

2025-03-05T13:05:56Z

Calvin Chau:

{{Publikation Erster Autor
|ErsterAutorVorname=Calvin
|ErsterAutorNachname=Chau
|FurtherAuthors=Jan Křetínský; Stefanie Mohr
}}
{{Inproceedings
|Referiert=0
|Title=Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks
|To appear=0
|Year=2023
|Booktitle=Automated Technology for Verification and Analysis
|Pages=401--421
|Publisher=Springer Nature Switzerland
|Editor=André, Étienne and Sun, Jun
}}
{{Publikation Details
|Abstract=Abstraction is a key verification technique to improve scalability. However, its use for neural networks is so far extremely limited. Previous approaches for abstracting classification networks replace several neurons with one of them that is similar enough. We can classify the similarity as defined either syntactically (using quantities on the connections between neurons) or semantically (on the activation values of neurons for various inputs). Unfortunately, the previous approaches only achieve moderate reductions, when implemented at all. In this work, we provide a more flexible framework, where a neuron can be replaced with a linear combination of other neurons, improving the reduction. We apply this approach both on syntactic and semantic abstractions, and implement and evaluate them experimentally. Further, we introduce a refinement method for our abstractions, allowing for finding a better balance between reduction and precision.
|DOI Name=10.1007/978-3-031-45329-8_19
|Projekt=SEMECO-Q2
|Forschungsgruppe=Verifikation und formale quantitative Analyse
}}

Inproceedings3474879216

2025-03-05T13:05:11Z

Calvin Chau:

{{Publikation Erster Autor
|ErsterAutorVorname=Christel
|ErsterAutorNachname=Baier
|FurtherAuthors=Calvin Chau; Sascha Klüppelholz
}}
{{Inproceedings
|Referiert=0
|Title=Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes
|To appear=0
|Year=2024
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9-13, 2024, Proceedings
|Pages=1--18
|Publisher=Springer
|Editor=Jane Hillston and Sadegh Soudjani and Masaki Waga
|Series=Lecture Notes in Computer Science
|Volume=14996
}}
{{Publikation Details
|Abstract=Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding witness. The certificate can be used to easily validate the correctness of the result and the witness provides useful diagnostic information, e.g. for debugging purposes. Thus, certificates and witnesses substantially increase the trustworthiness and understandability of the verification process. In this work, we consider certificates and witnesses for multi-objective reachability-invariant and mean-payoff queries in Markov decision processes, that is conjunctions or disjunctions either of reachability and invariant or mean-payoff predicates, both universally and existentially quantified. Thereby, we generalize previous works on certificates and witnesses for single reachability and invariant constraints. To this end, we turn known linear programming techniques into certifying algorithms and show that witnesses in the form of schedulers and subsystems can be obtained. As a proof-of-concept, we report on implementations of certifying verification algorithms and experimental results.
|DOI Name=10.1007/978-3-031-68416-6_1
|Projekt=SEMECO-Q2
|Forschungsgruppe=Verifikation und formale quantitative Analyse
}}