みなさま,
こんにちは! 東京大学の蓮尾です.
7月のバークレー,CAV 併設ワークショップ LfSA のご案内です.
- (***New!***) 締切りが延長されて,
Abstract submission: April 27
Paper submission: May 4
となりました.
- トピックは(広い意味での)論理を用いたシステム検証で,
- まだ新しいワークショップ(2回目)で正式なプロシーディングス
もありませんが,専門家が集うので「出席して役に立つ」会合である
と考えます.ぜひ投稿をご検討ください.(3カテゴリあります)
それでは!
蓮尾 一郎
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
================================================
Call for Papers
--------------------------------------------------
LfSA'12 -- Logics for System Analysis
http://www.ls.cs.cmu.edu/LfSA12
--------------------------------------------------
Workshop Affiliated with CAV 2012
July 7th, 2012, Berkeley, USA
Safety-critical systems frequently occur as real-time systems,
embedded systems, hybrid systems, distributed systems, and
cyber-physical systems. They are also becoming more and more important
in many application domains, including aviation, automotive, railway,
robotic, or medical applications, where both safety and security are
relevant aspects. To ensure the correct functioning of safety-critical
systems it is necessary to model and reason about hardware, software,
communication aspects, physical properties, and the system
environment.
LfSA’12 is the second workshop on Logics for System Analysis, devoted
to the systematic theoretical study, practical development, and
applied use of logics for system analysis. The purpose of the LfSA
workshop is to bring together researchers and practitioners interested
in studying practically relevant systems or in developing the logical
foundations and analysis tools for their study.
Topics include
* Logics for safety-critical systems (real-time, embedded, hybrid,
distributed, stochastic, cyber-physical)
* Logic-based methods for development of safety-critical systems
* Logics to study security aspects of systems or protocols
* System representations using logics, automata, modeling languages,
state charts, Petri nets, dataflow models
* Theories, decision procedures, and calculi for system analysis
* Model checking, theorem proving, and systematic testing
* Case studies for logical system analysis
* Applications of system analysis to industrial problems
In particular, we invite contributions that bridge the gap between
theory and practice or that combine different application domains.
Submission Categories
---------------------
* Regular papers (up to 15 pages), which should present previously
unpublished work (completed or in progress), including descriptions
of research, tools, and applications.
* Short papers (up to 5 pages), which describe work in progress or aim
at initiating discussions.
* Presentation-only papers, i.e., papers already submitted or
presented at a conference or another workshop; such papers will not
be included in the LfSA proceedings but will be presented during the
workshop.
In addition to informal and electronic workshop proceedings, we
consider the option of a special issue in a journal after the workshop
Workshop/Programme Chairs
-------------------------
Andre Platzer
Carnegie Mellon University
Philipp Ruemmer
Uppsala University
Programme Committee
-------------------
A. Banerjee (IMDEA Madrid)
R. Barbosa (U. Coimbra)
F. S. de Boer (CWI Amsterdam)
A. Cimatti (IRST Trento)
M. Dam (KTH Stockholm)
S. Demri (CNRS Cachan)
M. Giese (U. of Oslo)
I. Hasuo (U. Tokyo)
F. Ivancic (NEC Lab. Princeton)
E. B. Johnsen (U. of Oslo)
V. Sofronie-Stokkermans (U. Koblenz)
U. Waldmann (MPI Saarbrücken)
Important Dates/Deadlines
-------------------------
Abstract submission: April 27
Paper submission: May 4
Notification: June 8, 2012
Final version: June 29, 2012
Workshop: July 7, 2012
Workshop Webpage
----------------
http://www.ls.cs.cmu.edu/LfSA12
Submission via Easychair
------------------------
https://www.easychair.org/conferences/?conf=lfsa12
Logic, Algebra and Truth Degrees 2012
http://www.jaist.ac.jp/rcis/latd12/
Extension of deadline
=== EXTENDED Deadline for contributed talks: 29 April 2012 ===
=== Grants for travel available - please apply! ===
The deadline for submissions to LATD 2012 has been extended to
29 April 2012
Please hurry to submit your abstract (2-4 pages) at
http://www.easychair.org/conferences/?conf=latd2012
Travel/Participation grants
===========================
If there are economical reasons *not* to submit a contribution to the
conference, please consider applying for a grant with the following
information to latd12(a)jaist.ac.jp:
- name, affilitation
- amount of money needed
- title of your contribution (no grant without presentation)
- reason/explanation of need for grant
We will let you know the result of our decision on grant support
soon after the decision on the contributions.
========== Original Call for Contributions follows ==============
The third official meeting of the EUSFLAT Working Group on Mathematical
Fuzzy Logic [1] will be held on 10-14 September 2012 in Kanazawa, Japan.
The conference is organized by Research Center for Integrated Science
[2],
Japan Advanced Institute of Science and Technology [3].
Mathematical Fuzzy Logic is a subdiscipline of Mathematical Logic which
studies the notion of comparative truth. The assumption that 'truth
comes
in degrees' has proved to be very useful in many, both theoretical and
applied, areas of Mathematics, Computer Science and Philosophy.
The main goal of this meeting is to foster collaboration between
researchers in the area of Mathematical Fuzzy Logic, and to promote
communication and cooperation with members of neighbouring fields.
The featured topics include, but are not limited to, the following:
. Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction,
tableaux, resolution, computational complexity, etc.
. Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras,
MV-algebras, Abstract Algebraic Logic, functional representation, etc.
. Game-theory: Giles games, Rényi-Ulam games, evaluation games, etc.
. First-order fuzzy logics: axiomatizations, arithmetical hierarchy,
model theory, etc.
. Higher-order fuzzy logical systems: type theories, Fuzzy Class Theory,
and formal fuzzy mathematics.
. Philosophical issues: connections with vagueness and uncertainty.
. Applied fuzzy logical calculi: foundations of logical programming,
logic-based reasoning about similarity, description logics, etc.
We also welcome contributions on any relevant aspects of related logical
systems (such as substructural and quantum logics, and many-valued
logics
in general).
Conference Web Site:
http://www.jaist.ac.jp/rcis/latd12/
Important dates:
. 22 April 2012: deadline for submissions
. 3 June 2012: notifications sent
. 10-14 September 2012: conference
Programme Committee:
. Stefano Aguzzoli (University of Milano, Italy)
. Matthias Baaz (Vienna University of Technology, Austria)
. Petr Cintula (Academy of Sciences, Czech Republic)
. Carles Noguera (CSIC, Spain)
. Hiroakira Ono (JAIST, Japan), Chair
. James Raftery (University of KwaZulu-Natal, South Africa)
. Constantine Tsinakis (Vanderbilt University, USA)
Invited Speakers:
. Rostislav Horčík (Academy of Sciences, Czech Republic)
. Emil Jeřábek (Academy of Sciences, Czech Republic)
. Daniele Mundici (University of Florence, Italy)
. Greg Restall (University of Melbourne, Australia)
. Luca Spada (University of Salerno, Italy)
Tutorial:
. Felix Bou (University of Barcelona, Spain)
If you are interested in presenting a paper, please submit a 2-4 pages
abstract at
http://www.easychair.org/conferences/?conf=latd2012
Your submission will be confirmed automatically on the e-mail address
you provide. The accepted abstracts will be available on-line
after the final decision of the program committee. If you have any
problems to submit an abstract, please contact us at mail to:
latd2012(a)jaist.ac.jp
The deadline for contributions is 22 April 2012. The notification of
acceptance/rejection will be sent until 3 June 2012.
Registration:
Registration has not started by now, but we appreciate your email
informing us on your participation plans. Registration fee is likewise
not determined by now.
Grants:
There is a limited amount of grants available for participants. Please
contact us as soon as possible including the following information:
- name, affilitation
- amount of money needed
- title of your contribution (no grant without presentation)
- reason/explanation of need for grant
Conference dates:
The scientific program will start Monday morning (10 September) and
finish
Friday noon (14 September). Wednesday afternoon we plan an excursion.
Venue:
The conference will be held in the city of Kanazawa [4,5,6], located
in the
Ishikawa prefecture of Japan on the Japan Sea.
The venue is the Ishikawa Prefectural Museum of Art [7] in the center
of Kanazawa.
Local Organizing Committee:
. Norbert Preining (JAIST, Japan), Chair
. Katsuhiko Sano (JAIST, Japan)
. Kazushige Terui (Kyoto University, Japan)
. Shunsuke Yatabe (AIST, Japan)
For further information please contact: latd2012(a)jaist.ac.jp
[1] http://www.mathfuzzlog.org/
[2] http://www.jaist.ac.jp/rcis/en/
[3] http://www.jaist.ac.jp/
[4] http://en.wikipedia.org/wiki/Kanazawa,_Ishikawa
[5] http://www.kanazawa-tourism.com/
[6] http://wikitravel.org/en/Kanazawa
[7] http://www.ishibi.pref.ishikawa.jp/index_j.html
The third「論数哲」"Ron-Suu-Tetsu" (PhilLogMath) workshop
We will hold the 3rd 「論数哲」(PhilLogMath) workshop.
Our aim is to provide opportunities of detailed discussions among
philosophers, logicians, mathematicians and linguists.
We focus on theoretical and computational linguistics this time.
Everyone is welcome.
Date : May 17 (Thu)
Place: Seiryo Kaikan (Nagata-cho, Tokyo)
http://metropolis.co.jp/listings/venues/type/stage-venue/seiryo-kaikan/
Speaker:
*Daisuke Bekki (Ochanomizu University) and Hiroko Ozaki
(Ochanomizu University),
*Chung-chieh Shan (Cornell Unversity/ Tsukuba
University)
Two afternoon slots consists of 60 minutes talk and 30 minutes
discussion basically. Author meets Critics meeting is in Japanese, and
two afternoon talks are in English.
The details will be updated at our website url:
http://researchmap.jp/jopmokbbr-21098/#_21098
Workshop organizer (please replace [at] to @):
* Yuko Murakami
* Shunsuke Yatabe ( shunsuke.yatabe[at]aist.go.jp )
* Takuro Onishi ( takuro.onishi[at]gmail.com )
皆様
合流性 (チャーチ・ロッサ性) に関するワークショップ IWC 2012 の参加者募集と
合流性自動証明ツールのコンペティション CoCo 2012 の参加ツール募集
の案内をお知らせ致します。IWCの早期参加申し込み締切りは4月25日になって
おります。
廣川 直(北陸先端科学技術大学院大学)
======================================================================
Call for Participation
IWC 2012
1st International Workshop on Confluence
29 May 2012, Nagoya, Japan, collocated with RTA 2012
http://cl-informatik.uibk.ac.at/events/iwc-2012/
======================================================================
Recently there is a renewed interest in confluence research, resulting
in new techniques, tool support as well as new applications. The
workshop aims at promoting further research in confluence and related
properties. The workshop is collocated with the 23rd International
Conference on Rewriting Techniques and Applications (RTA 2012). During
the workshop the 1st Confluence Competition (CoCo 2012) takes place
(see below).
IMPORTANT DATES:
* early registration April 25, 2012 JST (GMT+9)
* registration May 9, 2012 JST (GMT+9)
* workshop May 29, 2012 JST (GMT+9)
Please register at:
https://apollon.nta.co.jp/rta2012/
INVITED SPEAKERS:
* Vincent van Oostrom Utrecht University
* Yoshihito Toyama Tohoku University
ACCEPTED PAPERS:
* Bertram Felgenhauer:
A Proof Order for Decreasing Diagrams
* Dominik Klein and Nao Hirokawa:
Confluence of Non-Left-Linear TRSs via Relative Termination (Extended Abstract)
* Christian Nemeth, Harald Zankl and Nao Hirokawa:
IaCOP - Interface for the Administration of COPS
* Kristoffer Rose:
A Case for Completion Modulo Equivalence
* Thomas Sternagel, René Thiemann, Harald Zankl and Christian Sternagel:
Recording Completion for Finding and Certifying Proofs in Equational Logic
* Hans Zantema:
Automatically Finding Non-Confluent Examples in Abstract Rewriting
ORGANISING COMMITTEE:
* Nao Hirokawa JAIST
* Aart Middeldorp University of Innsbruck
* Naoki Nishida Nagoya University
======================================================================
Second Call for Provers
CoCo 2012
1st Confluence Competition
http://coco.nue.riec.tohoku.ac.jp/2012/
======================================================================
Recently, several new implementations of confluence proving/disproving
tools are reported and interest for proving/disproving confluence
"automatically" has been grown. CoCo aims to foster the development of
techniques for proving/disproving confluence automatically by setting
up a dedicated and fair confluence competition among confluence
proving/disproving tools.
The 1st Confluence Competition (CoCo 2012) runs during the 1st
International Workshop on Confluence (IWC 2012), which is collocated
with the 23rd International Conference on Rewriting Techniques and
Applications (RTA 2012) at Nagoya University, Japan. In this
competition a category for first-order term rewrite systems will be
run. Other categories (e.g., higher-order) will be considered if there
are tools and problems.
IMPORTANT DATES:
* registration April 1, 2012 - May 15, 2012
* system description April 15, 2012 - May 15, 2012
* tool submission May 1, 2012 - May 15, 2012
* competition May 29, 2012
REGISTRATION/SUBMISSION:
Registration and tool submission will be via the email address:
coco-sc [AT] jaist.ac.jp
Tools must be able to read input files written in the old TPDB format.
The output of the tools must contain an answer in the first line
followed by some proof argument understandable for human experts.
Valid answers are YES (the input is confluent) and NO (the input is
not confluent). Every other answer is interpreted as the tool could
not determine the status of the input. For more information including
competition rules, see
http://coco.nue.riec.tohoku.ac.jp/
All registered tool authors are asked to submit a one-page system
description paper in EasyChair style. Submission is via EasyChair at
https://www.easychair.org/account/signin.cgi?conf=iwc2012
These papers will appear in the proceedings of IWC 2012.
ORGANISING COMMITTEE:
* Takahito Aoto Tohoku University (chair)
* Nao Hirokawa JAIST
* Harald Zankl University of Innsbruck
Please distribute this call to everybody you think intrested in.
======================================================
European PhD Program in Computational Logic (EPCL)
======================================================
http://www.epcl-study.eu/
CALL FOR APPLICATIONS
The European PhD Program in Computational Logic (EPCL) is run jointly
by four of the leading European universities in the field:
- Free University of Bozen-Bolzano (Italy),
- Technische Universität Dresden (Germany),
- Technische Universität Wien (Austria), and
- Universidade Nova de Lisboa (Portugal).
Further international universities, research organizations and
enterprises which contribute to Computational Logic or apply results
from it are involved as associated partners: The Simon Fraser
University (Canada), the Universidad de Chile, the National ICT
Australia Limited (NICTA), and several companies.
The program involves three years of PhD study in at least two of the
European partner universities. It leads to a joint doctoral degree of
the partner universities at which the studies have been physically
performed. The language of the program is English. Financial support
is available in the form of positions and scholarships.
Necessary requirements for participation in EPCL are a Master's degree
in Computer Science or Mathematics, or an equivalent degree; the proof
of adequate knowledge of English; and substantial knowledge in the
areas Foundations of Logics, Foundations of Artificial Intelligence
and Declarative Programming.
The program starts annually in the winter term. Applications for 2012
have to be electronically submitted on the Webpage
http://www.epcl-study.eu/, before the
=======================================
Application Deadline on 15 May 2012
=======================================
If you have enquiries, please do not hesitate to contact the
coordinator of the program
Prof. Steffen Hölldobler
Technische Universität Dresden
Fakultät Informatik
International Center for Computational Logic
Email: sh(a)iccl.tu-dresden.de
Phone: +49 (351) 463 38340
EPCL is supported by the German Federal Ministry of Education and
Research (BMBF) within the German Academic Exchange Service (DAAD)
program International Doctorates in Germany (IPID).
--
Dr.rer.nat.habil. Bertram Fronhöfer
TU Dresden
Department of Computer Science
International Center for Computational Logic
01062 Dresden, Germany
Tel.: +49 (0)351 463 39095
セミナーのご案内
日時:4月19日(木)16:30から
場所:東京工業大学 大岡山西8号館W棟11階 W1101セミナー室
会場までの交通案内はこちらから:
http://www.titech.ac.jp/about/campus/index.html
話者:蓮尾 一郎 (東京大学コンピュータ科学専攻)
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
題目:Programming with Infinitesimals: A While-Language for Hybrid System Modeling
(Joint Work with Kohei Suenaga, Kyoto University)
概要:
We add, to the common combination of a WHILE-language and a
Hoare-style program logic, a constant dt that represents an
infinitesimal (i.e. infinitely small) value. The outcome is a
framework for modeling and verification of hybrid systems: hybrid
systems exhibit both continuous and discrete dynamics and getting them
right is a pressing challenge. We rigorously define the semantics of
programs in the language of nonstandard analysis, on the basis of
which the program logic is shown to be sound and relatively complete.
If the time allows, our recent prototype automatic prover will also be
demonstrated.
参考文献:
Kohei Suenaga and Ichiro Hasuo.
Programming with Infinitesimals: A While-Language for Hybrid System Modeling.
Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.
Ichiro Hasuo and Kohei Suenaga.
Exercises in Nonstandard Static Analysis of Hybrid Systems.
To appear in Proc. CAV 2012.
問い合わせ先:
鹿島 亮(東京工業大学 数理・計算科学専攻)
kashima(a)is.titech.ac.jp
$B3'MM!"(B
$B:#=5$NLZMK$K5~Bg$G(BPaul-Andre Mellies$B$5$s$N9V1i$rM=Dj$7$F$$$^$9!#(B
$B4X?4$r$*;}$A$NJ}$O$I$&$>$*5$7Z$K$4;22C$/$@$5$$!#(B
$BD9C+@n???M(B
$B5~ETBg3X?tM}2r@O8&5f=j(B
------
$BF|;~(B: 19 April 2012 (Thursday) 11:00-12:00
$B>l=j(B: $B5~ETBg3XAm9g8&5f(B2$B9f4[(B478$B9f<<(B
Room 478, General Research Building No.2, Kyoto University
(Access information & map:
http://www.kyoto-u.ac.jp/en/accesshttp://www.kurims.kyoto-u.ac.jp/~hassei/map-2.jpg )
$B9V1i<T(B: Paul-Andre Mellies (CNRS, Paris VII)
$BBj(B: Braided notions of dialogue categories
$B35MW(B:
A dialogue category is a monoidal category equipped with an
exponentiating object. In this talk, I will introduce a notion
of braided dialogue category, and explain how this notion
provides a functorial bridge between proof theory and knot
theory.
($BLd$$9g$o$;(B: $BD9C+@n(B <hassei(a)kurims.kyoto-u.ac.jp>)
--
Masahito Hasegawa
Research Institute for Mathematical Sciences, Kyoto University
みなさま,
こんにちは! 東京大学の蓮尾と申します.
急なご案内ですが,講演を2件,お知らせさせてください.
木曜日のご講演は暗号理論の専門家によるものですが,内容は
暗号プロトコルの形式検証(計算論的安全性)に動機づけられた
ものです.形式検証の人向けに話してもらえるよう,お願いしてあります.
金曜日は線形論理・ゲーム意味論の専門家によるご講演です.
NII でも明日お話されるようですので,ぜひあわせてどうぞ.
会場のアクセスは,
http://www-mmm.is.s.u-tokyo.ac.jp/index.html
をご覧下さい.
みなさまのお越しをお待ちしております.それでは!
蓮尾 一郎
東京大学 コンピュータ科学専攻
http://www-mmm.is.s.u-tokyo.ac.jp
Thu 12 Apr 2012, 16:40-18:10
David Galindo <http://www.dgalindo.es/> (U. Luxembourg),
Encryption Schemes Secure in the Presence of Key Cycles
理学部7号館5階 511教室 Room 511, School of Science Bldg. No. 7
Traditionally the security of encryption schemes has relied
on the assumption that the decryption keys are not accessible to the
attacker neither directly (e.g. some parts of the decryption key might
have been leaked) nor indirectly (e.g. never encrypt messages that
depend on the decryption key). However this assumption has been
challenged in different contexts in the last decade. The main sources
have been side-channel attacks and formal cryptography.
In this talk we will give an introduction to the traditional security
notions for encryption schemes as well as the new notion of security
in the presence of key cycles. We will explain why the latter notion
is difficult to achieve using previous techniques. Finally we will
introduce the first practical encryption scheme achieving the latter
security notion (appeared at CRYPTO 2008).
Fri 13 Apr 2012, 16:40-18:10
Paul-Andre Mellies <http://www.pps.jussieu.fr/%7Emellies/> (U. Paris VII),
Tensorial logic: a type-theoretic foundation for game semantics
理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7
Tensorial logic is a primitive logic of tensor and negation which refines
linear logic by relaxing the hypothesis that negation is involutive. I will
explain how the logic provides a type-theoretic foundation to game
semantics, and how it may be extended with algebraic effects in order to
recover specific categories of games and strategies.