{"id":1460,"date":"2017-05-04T12:47:15","date_gmt":"2017-05-04T10:47:15","guid":{"rendered":"http:\/\/synasc.ro\/2017\/?page_id=1460"},"modified":"2017-07-04T16:05:09","modified_gmt":"2017-07-04T14:05:09","slug":"armin-biere","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2017\/invited-speakers-2\/armin-biere\/","title":{"rendered":"Armin Biere"},"content":{"rendered":"

Armin Biere
\n<\/strong>Johannes Kepler University, Linz, Austria<\/h2>\n

Title:\u00a0<\/em>Challenges in Verifying Arithmetic Circuits Using Computer Algebra<\/strong>
\n<\/em><\/p>\n

ABSTRACT:<\/strong><\/p>\n

Verifying arithmetic circuits such as multipliers and related circuits used to implement arithmetic units in processors or cryptographic functions remains an important problem, but in practice still requires
\nsubstantial manual effort.\u00a0 Out-of-the-box SAT solving does not work. It was even conjectured that proving such properties requires exponential resolution proofs.\u00a0 In this talk we want to focus on another line of research, which is applying computer algebra to verify properties of such circuits, most prominently properties of multiplier circuits. A recent approach based on polynomial reasoning made substantial progress in this regard.\u00a0 We are revisiting this approach, improve on some key aspects, and also lay out some future work.<\/p>\n

SHORT BIO:<\/strong><\/p>\n

\n

Since 2004\u00a0Prof.\u00a0Armin Biere<\/a>\u00a0is a Full Professor for Computer Science at the\u00a0Johannes Kepler University<\/a>\u00a0in Linz, Austria, and chairs the\u00a0Institute for Formal Models and Verification<\/a>.<\/p>\n

Between 2000 and 2004 he held a position as Assistant Professor within the\u00a0Department of Computer Science<\/a>\u00a0at\u00a0ETH Z\u00fcrich<\/a>, Switzerland. In 1999 Biere was working for a start-up company in electronic design automation after one year as Post-Doc with\u00a0Edmund Clarke<\/a>\u00a0at\u00a0CMU<\/a>, Pittsburgh, USA. In 1997 Biere received a Ph.D. in\u00a0Computer Science<\/a>\u00a0from the\u00a0University of Karlsruhe<\/a>, Germany.<\/p>\n

His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques. He is the author and co-author of more than 120 papers and served on the program committee of more than 110 international conferences and workshops. His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 57 medals including 32 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential in the first 20 years of TACAS in 2014, and the ETAPS 2017 Test of Time Award.<\/p>\n

Besides organizing several workshops Armin Biere was co-chair of\u00a0SAT’06<\/a>, and\u00a0FMCAD’09<\/a>, was PC co-chair of\u00a0HVC’12<\/a>, and co-chair of\u00a0CAV’14<\/a>. He serves on the editorial boards of the\u00a0Journal on Satisfiability, Boolean Modeling and Computation (JSAT)<\/a>, the\u00a0Journal of Automated Reasoning (JAR)<\/a>, and the journal for\u00a0Formal Methods in System Design (FMSD)<\/a>.<\/p>\n

He is an editor of the\u00a0Handbook of Satisfiability<\/a>\u00a0and initiated and organizes the\u00a0Hardware Model Checking Competition (HWMCC)<\/a>. Since 2011 he serves as chair of the\u00a0SAT Association<\/a>\u00a0and since 2012 on the steering committee of\u00a0FMCAD<\/a>. In 2006 Armin Biere co-founded\u00a0NextOp Software Inc.<\/a>\u00a0which was acquired by\u00a0Atrenta Inc.<\/a>\u00a0in 2012.<\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

Armin Biere Johannes Kepler University, Linz, Austria Title:\u00a0Challenges in Verifying Arithmetic Circuits Using Computer Algebra ABSTRACT: Verifying arithmetic circuits such as multipliers and related circuits used to implement arithmetic units in processors or cryptographic functions remains an important problem, but in practice still requires substantial manual effort.\u00a0 Out-of-the-box SAT solving does not work. It was […]<\/p>\n","protected":false},"author":4,"featured_media":0,"parent":613,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1460","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/pages\/1460","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/comments?post=1460"}],"version-history":[{"count":4,"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/pages\/1460\/revisions"}],"predecessor-version":[{"id":1556,"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/pages\/1460\/revisions\/1556"}],"up":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/pages\/613"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2017\/wp-json\/wp\/v2\/media?parent=1460"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}