• Zum Inhalt springen (Accesskey 1)
  • Zur Suche springen (Accesskey 7)
FWF — Österreichischer Wissenschaftsfonds
  • Zur Übersichtsseite Entdecken

    • Forschungsradar
      • Historisches Forschungsradar 1974–1994
    • Entdeckungen
      • Emmanuelle Charpentier
      • Adrian Constantin
      • Monika Henzinger
      • Ferenc Krausz
      • Wolfgang Lutz
      • Walter Pohl
      • Christa Schleper
      • Elly Tanaka
      • Anton Zeilinger
    • Impact Stories
      • Verena Gassner
      • Wolfgang Lechner
      • Birgit Mitter
      • Oliver Spadiut
      • Georg Winter
    • scilog-Magazin
    • Austrian Science Awards
      • FWF-Wittgenstein-Preise
      • FWF-ASTRA-Preise
      • FWF-START-Preise
      • Auszeichnungsfeier
    • excellent=austria
      • Clusters of Excellence
      • Emerging Fields
    • Im Fokus
      • 40 Jahre Erwin-Schrödinger-Programm
      • Quantum Austria
      • Spezialforschungsbereiche
    • Dialog und Diskussion
      • think.beyond Summit
      • Am Puls
      • Was die Welt zusammenhält
      • FWF Women’s Circle
      • Science Lectures
    • Wissenstransfer-Events
    • E-Book Library
  • Zur Übersichtsseite Fördern

    • Förderportfolio
      • excellent=austria
        • Clusters of Excellence
        • Emerging Fields
      • Projekte
        • Einzelprojekte
        • Einzelprojekte International
        • Klinische Forschung
        • 1000 Ideen
        • Entwicklung und Erschließung der Künste
        • FWF-Wittgenstein-Preis
      • Karrieren
        • ESPRIT
        • FWF-ASTRA-Preise
        • Erwin Schrödinger
        • doc.funds
        • doc.funds.connect
      • Kooperationen
        • Spezialforschungsgruppen
        • Spezialforschungsbereiche
        • Forschungsgruppen
        • International – Multilaterale Initiativen
        • #ConnectingMinds
      • Kommunikation
        • Top Citizen Science
        • Wissenschaftskommunikation
        • Buchpublikationen
        • Digitale Publikationen
        • Open-Access-Pauschale
      • Themenförderungen
        • AI Mission Austria
        • Belmont Forum
        • ERA-NET HERA
        • ERA-NET NORFACE
        • ERA-NET QuantERA
        • Ersatzmethoden für Tierversuche
        • Europäische Partnerschaft BE READY
        • Europäische Partnerschaft Biodiversa+
        • Europäische Partnerschaft BrainHealth
        • Europäische Partnerschaft ERA4Health
        • Europäische Partnerschaft ERDERA
        • Europäische Partnerschaft EUPAHW
        • Europäische Partnerschaft FutureFoodS
        • Europäische Partnerschaft OHAMR
        • Europäische Partnerschaft PerMed
        • Europäische Partnerschaft Water4All
        • Gottfried-und-Vera-Weiss-Preis
        • LUKE – Ukraine
        • netidee SCIENCE
        • Projekte der Herzfelder-Stiftung
        • Quantum Austria
        • Rückenwind-Förderbonus
        • WE&ME Award
        • Zero Emissions Award
      • Länderkooperationen
        • Belgien/Flandern
        • Deutschland
        • Frankreich
        • Italien/Südtirol
        • Japan
        • Korea
        • Luxemburg
        • Polen
        • Schweiz
        • Slowenien
        • Taiwan
        • Tirol-Südtirol-Trentino
        • Tschechien
        • Ungarn
    • Schritt für Schritt
      • Förderung finden
      • Antrag einreichen
      • Internationales Peer-Review
      • Förderentscheidung
      • Projekt durchführen
      • Projekt beenden
      • Weitere Informationen
        • Integrität und Ethik
        • Inklusion
        • Antragstellung aus dem Ausland
        • Personalkosten
        • PROFI
        • Projektendberichte
        • Projektendberichtsumfrage
    • FAQ
      • Projektphase PROFI
      • Projektphase Ad personam
      • Auslaufende Programme
        • Elise Richter und Elise Richter PEEK
        • FWF-START-Preise
  • Zur Übersichtsseite Über uns

    • Leitbild
    • FWF-Film
    • Werte
    • Zahlen und Daten
    • Jahresbericht
    • Aufgaben und Aktivitäten
      • Forschungsförderung
        • Matching-Funds-Förderungen
      • Internationale Kooperationen
      • Studien und Publikationen
      • Chancengleichheit und Diversität
        • Ziele und Prinzipien
        • Maßnahmen
        • Bias-Sensibilisierung in der Begutachtung
        • Begriffe und Definitionen
        • Karriere in der Spitzenforschung
      • Open Science
        • Open-Access-Policy
          • Open-Access-Policy für begutachtete Publikationen
          • Open-Access-Policy für begutachtete Buchpublikationen
          • Open-Access-Policy für Forschungsdaten
        • Forschungsdatenmanagement
        • Citizen Science
        • Open-Science-Infrastrukturen
        • Open-Science-Förderung
      • Evaluierungen und Qualitätssicherung
      • Wissenschaftliche Integrität
      • Wissenschaftskommunikation
      • Philanthropie
      • Nachhaltigkeit
    • Geschichte
    • Gesetzliche Grundlagen
    • Organisation
      • Gremien
        • Präsidium
        • Aufsichtsrat
        • Delegiertenversammlung
        • Kuratorium
        • Jurys
      • Geschäftsstelle
    • Arbeiten im FWF
  • Zur Übersichtsseite Aktuelles

    • News
    • Presse
      • Logos
    • Eventkalender
      • Veranstaltung eintragen
      • FWF-Infoveranstaltungen
    • Jobbörse
      • Job eintragen
    • Newsletter
  • Entdecken, 
    worauf es
    ankommt.

    FWF-Newsletter Presse-Newsletter Kalender-Newsletter Job-Newsletter scilog-Newsletter

    SOCIAL MEDIA

    • LinkedIn, externe URL, öffnet sich in einem neuen Fenster
    • , externe URL, öffnet sich in einem neuen Fenster
    • Facebook, externe URL, öffnet sich in einem neuen Fenster
    • Instagram, externe URL, öffnet sich in einem neuen Fenster
    • YouTube, externe URL, öffnet sich in einem neuen Fenster

    SCILOG

    • Scilog — Das Wissenschaftsmagazin des Österreichischen Wissenschaftsfonds (FWF)
  • elane-Login, externe URL, öffnet sich in einem neuen Fenster
  • Scilog externe URL, öffnet sich in einem neuen Fenster
  • en Switch to English

  

Algorithmische Analyse von nebenläufigen Systemen

Algorithmic Analysis of Concurrent Systems

Andreas Pavlogiannis (ORCID: 0000-0002-8943-0722)
  • Grant-DOI 10.55776/J4220
  • Förderprogramm Erwin Schrödinger
  • Status beendet
  • Projektbeginn 01.11.2018
  • Projektende 31.08.2019
  • Bewilligungssumme 135.240 €
  • Projekt-Website

Wissenschaftsdisziplinen

Informatik (100%)

Keywords

    Software Verification, Concurrency, Algorithms, St

Abstract Endbericht

Computersysteme sind heutzutage allgegenwärtig. Auf der einen Seite, übernimmt Software ständig neue, kritische Aufgaben, von Systemen für medizinische Assistenz bis zu selbstfahrenden Autos. Auf der anderen Seite, ist Software zu einem unverzichtbaren Teil unseres Alltags geworden, beispielsweise bei Kommunikationsdiensten, Smart-Home-Geräten, E-Business und Online-Banking-Transaktionen. Die zunehmende Nachfrage nach computergestützter Automatisierung bedingt die Notwendigkeit von formaler Verifikation. Es gibt immer die Möglichkeit eines Systemversagens, und je mehr die Gesellschaft auf diese Systeme angewiesen ist, desto schlimmer sind die Folgen des Versagens. Programmanalyse und verifikation ermöglichen es auf systematische Weise die Korrektheit von Programmen zu zeigen, und Programmfehler in einem frühen Entwicklungsstadium zu entdecken. Die Mehrheit der heutigen Systeme ist nebenläufig, bedingt durch Fortschritt in der Hardwareentwicklung von Multicore-Architekturen und durch dem zunehmenden Erfolg von Cloud-basierten Diensten. ine der größten Herausforderungen der Softwareentwicklung ist die Verifikation von nebenläufigen Programmen. Einerseits sind solche Programme aufgrund der inhärenten Komplexität, die sich aus den Wechselwirkungen der nebenläufigen Komponenten ergibt, notorisch schwierig korrekt zu schreiben. Andererseits ist ein fehlerhaftes Verhalten durch Tests schwer reproduzierbar, so dass man auf systematisches (formales) Beweisen angewiesen ist um die Korrektheit des Programms zu zeigen. Obwohl die nebenläufige Programmierung immer wichtig wird, sind noch viele Herausforderungen der nebenläufige Verifikation ungelöst. Darunter ist die Skalierbarkeit wohl das größte Problem: Wie können wir der exponentiellen Komplexitätssteigerung aufgrund des nebenläufigen Nicht-Determinismus Herr werden? Versuche der Komplexität mittels Optimierungen in der Software Herr zu werden sind nicht zielführend. Solche Versuche führen oft nur zu inkrementellen Verbesserungen, es fehlt eine solide theoretische Grundlage und ein genereller Ansatz. Zusätzlich entstehen durch die ständige Weiterentwicklung von nebenläufigen Systemen andauernd neue Herausforderungen, wie zum Beispiel verbesserte Kommunikationsmethoden und Verzögerungen bei der Synchronisation. Diese Herausforderungen dürfen nicht ungelöst bleiben. Es bedarf grundlegender Fortschritte damit die nebenläufige Verifikation praktisch anwendbar ist. Mein Vorschlag besteht darin, die Grundlagen der formale Verifikation von nebenläufigen Systemen zu studieren. Das Hauptziel ist neue Theorien und Algorithmen zu entwickeln, und das sekundäre Ziel ist die Entwicklung von neuen Tools, die auf den neuen Algorithmen aufbauen. Im Vergleich zu bestehenden Engineering Techniken, hat dieser Ansatz zwei Vorteile: Zum Ersten führt ein algorithmischer Ansatz zu starken, beweisbaren Garantien, die die neuen Methoden universell anwendbar machen. Zum Zweiten erfordern gute Algorithmen auch gute Theoreme um die Intuition zu formalisieren. Dies ist der beste Weg, damit der Bereich auf eine stabile Weise, über die inkrementellen Verbesserungen von Ad-hoc-Lösungen hinaus, vorankommen kann. Ein solcher Paradigmenwechsel wird eine solide Basis für neue Werkzeuge bieten, deren Anwendbarkeit über die inkrementelle Verbesserungen der technischen Implementierung allein, hinausgeht.

Das Projekt hat zu neue Methodologien in drei verschiedeneBereichen der Programmanalyse beitragt. Diese werden im Folgenden kurz beschrieben. Erstens, haben wir neue, effiziente Algorithmen zur Analyse des Speicherbedarfs von Programmen entwickelt. Der Speicherbedarf bezieht sich auf das Pattern der Speicherzugriffe, die ein Programm durchführt. Durch die Analyse dieses Patterns können wir die Speicherzugriffe, die von das Programm in der Zukunft vornehmen werden, vorhersagen und die Daten proaktiv abrufen, bevor sie, zum Beispiel, angefordert werden. Dieser Prozess führt zu einer Leistungsoptimierung, da das Programm einen direkten Zugriff auf die Daten hat, ohne lange Wartezeiten für die Datenübertragung von dem Speicher zu der CPU. Das Problem der Analyse des Speicherfootprints ist generell bekannt als ein unlenksames Problem zu sein. Im Rahmen unseres Projekts haben wir große Klassen von komplexen Programmen, wie zum Beispiel numerische Berechnungsprograme, identifiziert, für denen schnelle Algorithmen entwickelt konnten, wobei wir die bekannten schwerfälligen Ergebnisse für den allgemeinen Fall umgegangen haben. Zweitens, haben wir neue Algorithmen für die effiziente Verifikation von nebenläufigen Systeme entwickelt. Ein nebenläufiges System ist bekanntlich schwer zu analysieren, da es aufgrund des Zusammenwirkens seiner Komponenten ein unberechenbares Verhalten ausstellen kann. Das macht die Analyse der nebenläufigen Systeme zu einer ständigen Herausforderung. Im Rahmen unseres Projekts haben wir einen neuen Algorithmus entwickelt, der in der Lage ist, innerhalb berechtigten Zeitraum komplexere nebenläufige Programme als die bestehenden Techniken zu analysieren. Drittens, haben wir neue Algorithmen für die effiziente prädiktive Prüfung der nebenläufigen Systeme entwickelt. In Allgemeinen beschäftigt sich der Bereich der prädiktiven Prüfung mit der folgender Herausforderung: wenn wir die Ausführung eines nebenläufiges Programmes beobachten, bei der kein Fehler auftritt, können wir dann erkennen, ob eine andere ähnliche Ausführung zu einem Fehler führen würde? Obwohl dieser Ansatz im Allgemeinen keine Garantie für die Erkennung von Fehlern bietet, wird er häufiger verwendet als die Verifizierung von nebenläufigen Systemen, weil er in der Praxis aufgrund zeitlicher Beschränkungen leichter durchführbar ist. Im Rahmen unseres Projekts haben wir einen neuen, schnellen Algorithmus für die prädiktive Prüfung der nebenläufigen Systeme entwickelt. Im Vergleich zu bestehenden Techniken ist unser Algorithmus in der Lage den Begriff der Ähnlichkeit in Bezug auf die Referenzausführung zu entspannen und damit mehr Fehler als die bestehenden Techniken zu erkennen. Der Algorithmus wurde auf große und komplexe Programme angewendet und war in der Lage verschiedene Fehler zu erkennen, die schon existieren aber bisher unentdeckt geblieben waren.

Forschungsstätte(n)
  • École polytechnique fédérale de Lausanne - 100%

Research Output

  • 219 Zitationen
  • 6 Publikationen
Publikationen
  • 2019
    Titel Efficient parameterized algorithms for data packing
    DOI 10.1145/3290366
    Typ Journal Article
    Autor Chatterjee K
    Journal Proceedings of the ACM on Programming Languages
    Seiten 1-28
    Link Publikation
  • 2022
    Titel Infection dynamics of COVID-19 virus under lockdown and reopening
    DOI 10.1038/s41598-022-05333-5
    Typ Journal Article
    Autor Svoboda J
    Journal Scientific Reports
    Seiten 1526
    Link Publikation
  • 2019
    Titel Population structure determines the tradeoff between fixation probability and fixation time
    DOI 10.1038/s42003-019-0373-y
    Typ Journal Article
    Autor Tkadlec J
    Journal Communications Biology
    Seiten 138
    Link Publikation
  • 2019
    Titel Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth
    DOI 10.1145/3363525
    Typ Journal Article
    Autor Chatterjee K
    Journal ACM Transactions on Programming Languages and Systems (TOPLAS)
    Seiten 1-46
  • 2019
    Titel Fast, sound, and effectively complete dynamic race prediction
    DOI 10.1145/3371085
    Typ Journal Article
    Autor Pavlogiannis A
    Journal Proceedings of the ACM on Programming Languages
    Seiten 1-29
    Link Publikation
  • 2020
    Titel Limits on amplifiers of natural selection under death-Birth updating
    DOI 10.1371/journal.pcbi.1007494
    Typ Journal Article
    Autor Tkadlec J
    Journal PLOS Computational Biology
    Link Publikation

Entdecken, 
worauf es
ankommt.

Newsletter

FWF-Newsletter Presse-Newsletter Kalender-Newsletter Job-Newsletter scilog-Newsletter

Kontakt

Österreichischer Wissenschaftsfonds FWF
Georg-Coch-Platz 2
(Eingang Wiesingerstraße 4)
1010 Wien

office(at)fwf.ac.at
+43 1 505 67 40

Allgemeines

  • Jobbörse
  • Arbeiten im FWF
  • Presse
  • Philanthropie
  • scilog
  • Geschäftsstelle
  • Social Media Directory
  • LinkedIn, externe URL, öffnet sich in einem neuen Fenster
  • , externe URL, öffnet sich in einem neuen Fenster
  • Facebook, externe URL, öffnet sich in einem neuen Fenster
  • Instagram, externe URL, öffnet sich in einem neuen Fenster
  • YouTube, externe URL, öffnet sich in einem neuen Fenster
  • Cookies
  • Hinweisgeber:innensystem
  • Barrierefreiheitserklärung
  • Datenschutz
  • Impressum
  • IFG-Formular
  • Social Media Directory
  • © Österreichischer Wissenschaftsfonds FWF
© Österreichischer Wissenschaftsfonds FWF