Detailansicht

Wissensnetz

Person

Armin Biere (1967-)

Informatiker

Name	Armin Biere
Zeit	1967- (Lebensdaten)
Ort	Villingen im Schwarzwald (Geburtsort) Deutschland
Geschlecht	männlich
Akademischer Grad bzw. Titel	Prof. Dr.
Beruf	Informatiker (charakteristischer Beruf)
Beziehung	Albert-Ludwigs-Universität Freiburg (01.08.2021-) Johannes Kepler Universität Linz (Professor) (01.09.2004--31.07.2021)
Weitere Angaben	Dt. Informatiker, 1997 Promotion im Fach Informatik, Univ. Karlsruhe, seit 2004 Prof. an der Univ. Linz, Leiter des Inst. für Formale Modelle und Verifikation Informatiker
Quelle	Homepage: http://fmv.jku.at/biere/ Internet: http://de.wikipedia.org/wiki/Armin_Biere
Datensatztyp	Person
GND-Nummer	115751823
Datensatz-ID	115751823
Beteiligt an alle anzeigen Certified SAT solving with GPU accelerated inprocessing Clausal congruence closure Certified SAT solving with GPU accelerated inprocessing Mining definitions in Kissat with Kittens Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra Faster LRAT checking than solving with CaDiCaL Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra MBMV 2023 : Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen : 26. Workshop, 23.-24. März 2023 in Freiburg On safety verification using PDR and Reverse PDR Clausal proofs for pseudo-boolean reasoning Mining definitions in Kissat with Kittens Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020 AMULET 2.0 for verifying multiplier circuits Efficient All-UIP learned clause minimization Non-clausal redundancy properties SAT solving with GPU accelerated inprocessing Incremental column-wise verification of arithmetic circuits using computer algebra Strong Extension-Free Proof Systems Incremental column-wise verification of arithmetic circuits using computer algebra Strong Extension-Free Proof Systems Encoding Redundancy for Satisfaction-Driven Clause Learning Btor2 , BtorMC and Boolector 3.0 Local redundancy in SAT: generalizations of blocked clauses Propagation based local search for bit-precise reasoning Propagation based local search for bit-precise reasoning Hardware and Software: Verification and Testing : 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings Hardware and software: verification and testing : revised selected papers Efficiently representing existential dependency sets for expansion-based QBF solvers Digitaltechnik - eine praxisnahe Einführung Digitaltechnik - eine praxisnahe Einführung Compressing BMC encodings with QBF Liveness checking as safety checking for infinite state spaces Theory and applications of satisfiability testing : 9th international conference ; proceedings Theory and applications of satisfiability testing : 9th international conference, Seattle, WA, USA, August 12 - 15, 2006 ; proceedings Combined static and dynamic analysis JVM independent replay in java Subroutine inlining and bytecode abstraction to simplify static and dynamic analysis Formal methods group ETH Zürich Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function Liveness checking as safety checking Combining local and global model checking Combining local and global model checking Effiziente Modellprüfung des μ-Kalküls [my-Kalküls] mit binären Entscheidungsdiagrammen A case study on different modelling approaches based on model checking : verifying numerous versions of the alternating bit protocol with SMV

Hinweis

Die Betaversion beinhaltet noch nicht alle Funktionen und Informationen des Katalogs des DNB-Portals. Falls Sie Informationen vermissen oder ein Medium bestellen wollen, besuchen Sie bitte die entsprechende Seite im Katalog des DNB-Portals über folgenden Link:

Katalog der Deutschen Nationalbibliothek

Armin Biere (1967-)

Certified SAT solving with GPU accelerated inprocessing

Clausal congruence closure

Certified SAT solving with GPU accelerated inprocessing

Mining definitions in Kissat with Kittens

Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra

Faster LRAT checking than solving with CaDiCaL

Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra

MBMV 2023 : Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen : 26. Workshop, 23.-24. März 2023 in Freiburg

On safety verification using PDR and Reverse PDR

Clausal proofs for pseudo-boolean reasoning

Mining definitions in Kissat with Kittens

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020

AMULET 2.0 for verifying multiplier circuits

Efficient All-UIP learned clause minimization

Non-clausal redundancy properties

SAT solving with GPU accelerated inprocessing

Incremental column-wise verification of arithmetic circuits using computer algebra

Strong Extension-Free Proof Systems

Incremental column-wise verification of arithmetic circuits using computer algebra

Strong Extension-Free Proof Systems

Encoding Redundancy for Satisfaction-Driven Clause Learning

Btor2 , BtorMC and Boolector 3.0

Local redundancy in SAT: generalizations of blocked clauses

Propagation based local search for bit-precise reasoning

Propagation based local search for bit-precise reasoning

Hardware and Software: Verification and Testing : 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings

Hardware and software: verification and testing : revised selected papers

Efficiently representing existential dependency sets for expansion-based QBF solvers

Digitaltechnik - eine praxisnahe Einführung

Digitaltechnik - eine praxisnahe Einführung

Compressing BMC encodings with QBF

Liveness checking as safety checking for infinite state spaces

Theory and applications of satisfiability testing : 9th international conference ; proceedings

Theory and applications of satisfiability testing : 9th international conference, Seattle, WA, USA, August 12 - 15, 2006 ; proceedings

Combined static and dynamic analysis

JVM independent replay in java

Subroutine inlining and bytecode abstraction to simplify static and dynamic analysis

Formal methods group ETH Zürich

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

Liveness checking as safety checking

Combining local and global model checking

Combining local and global model checking

Effiziente Modellprüfung des μ-Kalküls [my-Kalküls] mit binären Entscheidungsdiagrammen

A case study on different modelling approaches based on model checking : verifying numerous versions of the alternating bit protocol with SMV