CAV 2013 Promo (RU)

 

Международная конференция

Computer Aided Verification 2013 (CAV 2013)

Автоматизированные методы верификации 2013

Санкт-Петербург, Россия


О верификации

Методы формального анализа – область прикладной математики, изучающая методы и алгоритмы проверки свойств сложных систем: аппаратного обеспечения, последовательных и параллельных программ. В качестве примера интересующих свойств можно представить те свойства программ, которые пользователи считают само собой разумеющимися: отклик программы на действия пользователя, отсутствие зацикливания программы, отсутствие эффектов аварийного завершения программы. В тех случаях, когда авторы системы могут сформулировать требования к системе в виде формальных спецификаций, говорят о верификации системы – математически строгой проверке того, что поведение системы соответствует выдвинутым требованиям. Процесс верификации даёт гарантию отсутствия в системе определённых ошибок, заключающихся в расхождении между спецификациями разработчика и возможным поведением системы. Такая гарантия особенно важна для технически сложных производственных систем, а также продуктов с большим кругом пользователей.

Несмотря на пессимистичный результат о завершаемости программ, полученный Аланом Тьюрингом на заре развития программирования, методы верификации развивались на протяжении последних 50 лет и прошли несколько этапов взросления. Так в 60-70-ых гг. прошлого века верификация представляла чисто академический интерес и не давала практической отдачи. В 80-90-ых гг. разработчики аппаратных систем стали внедрять методы верификации, в частности методы проверки моделей (model checking), в промышленность. Например, на сегодняшний день процессоры проходят несколько стадий формальной проверки свойств в процессе разработки. В начале 21-го века появились практически полезные средства анализа и верификации программ. Признанием ценности методов верификации в 2007 г. послужило вручение премии Тьюринга – аналога Нобелевской премии для программистов и математиков – авторам метода model checking: Эдмонду Кларку, Алану Эмерсону и Жозефу Сифакису.

Формальные методы нашли применение не только для проверки свойств критических и дорогостоящих систем. На практике методы также используются для: поиска ошибок в программах, систематического тестирования программ, анализа производственных процессов, поиска закономерностей в биологических системах, оценки информационной безопасности программ. В истории формальных методов конференция CAV несколько раз служила катализатором новых идей, открывавших неожиданные перспективы и способствующих успешному промышленному применению.

 

О конференции

CAV 2013 – двадцать пятая конференция, посвящённая теоретическим и практическим достижениям в области методов формального анализа аппаратных и программных систем. Для комитета конференции CAV крайне важны: сохранение лидирующих позиций в верификации аппаратных систем, поддержка недавно набранного темпа в верификации программных систем, а так же интерес к таким новым предметным областям, как биологические системы. Конференция охватывает темы от теоретических результатов до практических приложений, при этом уделяя особое внимание практически полезным средствам верификации, алгоритмам и методам, необходимым для их реализации. Труды конференции публикуются в издании «Springer-Verlag’s Lecture Notes in Computer Science».


Темы конференции включают:

  • методы верификации моделей (model checking);
  • алгоритмы и инструменты для верификации моделей и их реализаций;
  • методы верификации аппаратного обеспечения;
  • верификация гибридных и встроенных систем;
  • анализ программ и верификация программного обеспечения;
  • языки моделирования и спецификации;
  • методы абстракции, дедуктивных и композиционных рассуждений в верификации;
  • тестирование и анализ на этапе выполнения, основанные на методах верификации;
  • приложения и анализ отдельных примеров (case studies);
  • верификация в промышленности;
  • формальные методы в биологических системах.

В программные комитеты конференций последних лет входили известные исследователи в области методов верификации:
Edmund M. Clark (Carnegie Mellon Univ., USA), Orna Grumberg (Technion, Israel), Kenneth McMillan (Microsoft, USA), Robert P. Kurshan (Cadence, USA), Mike Gordon (Univ. of Cambridge, UK), Rajeev Alur (Univ. Of Pennsylvania, USA), Domagoj Babic (Synopsis, USA), Roderick Bloem (Graz Univ. of Technology, Austria), Ahmed Boujjani (Univ. of Paris 7, France), Alessandro Cimatti (FBK-irst, Italy), Javier Esparza (Technical Univ. of Munich, Germany), Azadeh Farzan (Univ. of Toronto, Canada), Martin Fraenzle (Carl von Ossietzky Univ. Oldenburg, Germany), Ganesh Gopalakrishnan (Univ. of Utah, USA), Susanne Graf (VERIMAG, France), Ziyad Hanna (Jasper, USA), Holger Hermanns (Saardland Univ., Germany), Alan Hu (Univ. of British Columbia, Canada), Kevin Jones (Green Plug, USA), Vineet Kahlon (NEC Laboratories, USA), Jean Krivine (PPS, France), Daniel Kroening (Oxford Univ., UK), Sava Krstic (Intel Corp., USA), Marta Kwiatkowska (Univ. of Oxford, UK), Kim Larsen (Aalborg Univ., Denmark), Orna Kupferman (Hebrew Univ.), Oded Maler (Verimag, France), David Monniaux (CNRS/VERIMAG, France), Markus Mueller-Olm (Westfaelische Wilhems-Universitaet Muenster, Germany), Kedar Namjoshi (Bell Labs, USA), Doron Peled (Bar Ilan Univ., Israel), Shaz Qadeer (Microsoft, USA), Jean-Francois Raskin (Brussels Univ., Belgium), Andrey Rybalchenko (Technical Univ. of Munich, Germany), Natasha Sharygina (Univ. of Lugano, Switzerland), Ofer Strichman (Technion, Israel), Helmut Veith (Vienna Univ. of Technology, Austria), Kwangkeun Yi (Seoul National Univ., Rep. of Korea), Karen Yorav (IBM Haifa Research Lab, Israel), Greta Yorsh (IBM, USA).

В рамках конференции проводятся смежные международные семинары:

Numerical Software Verification, SPIN on Model Checking of Software, Frontiers in Analog Circuit, Satisfiability Modulo Theories, Exploiting Concurrency Efficiently and Correctly, Parallel Distributed Methods in Verification, Formal Methods for Robotics and Automation, Practical Synthesis for Concurrent Systems.

Географический охват конференции:

Иллинойс (США), Юта (США), Эдинбург (Великобритания), Гренобль (Франция), Принстон (США), Берлин (Германия), Сиэттл (Канада), Бостон (США), Болдер (США), Копенгаген (Дания), Париж (Франция), Чикаго (США), Тренто (Италия), Ванкувер (Канада), Хайфа (Израиль), Нью Брунсвик (США), Льеж (Бельгия), Стэнфорд (США), Элунда (Греция), Монреаль (Канада), Аалборг (Дания).

Количество участников:
ежегодно около 50 докладчиков и 200 участников.

Сайты последних конференций (CAV 2009-2012):