皆様,
京都大学の末永と申します.
先日お知らせしましたハイブリッドシステムに関する
国際会議 HSCC 2014 の締切 (10月20日) まで一ヶ月を切りましたので,
再度 CFP をお送りします.アブストラクト締切が 10月13日です.
どうぞ投稿をご検討くださいませ.
末永幸平
--
18th International Conference on Hybrid Systems: Computation and Control
April 14-16, 2015, Seattle, USA.
URL: http://2015.hscc-conference.org/
Important dates
Abstract Submission deadline: October 13, 2014.
Full Paper Submission deadline: October 20, 2014. (no extensions possible).
Rebuttal phase: December 4 to December 7, 2014.
Author …
[View More]notification: December 17, 2014.
Camera-ready submission: February 3, 2015.
Conference dates: April 14-16, 2015.
Conference Scope
Hybrid Systems: Computation and Control (HSCC) has long been a
leading, single-track conference on foundations, techniques, and tools
for analysis, control, synthesis, implementation, and applications of
dynamical systems that exhibit continuous and discrete (hybrid)
dynamics. Applications include cyber-physical systems (CPS), mixed
signal circuits, robotics, large-scale infrastructure networks, as
well as natural systems such as biochemical and physiological
models. In particular, we solicit theoretical as well as applied
research papers that present original work combining ideas from
computer science and control systems.
Topics of interest include, but are not limited to:
- Design, synthesis and control
- Analysis and verification
- Computability and complexity
- Programming languages, specification formalisms
- Software tool engineering and experimentation
- Real-time and resource-aware control for embedded systems
- Network science and control over networks
- Applications in automotive, avionics, energy, mobile robotics,
medical devices, manufacturing, systems biology,
transportation, and other areas
HSCC 2015 will be part of the 8th CPSWeek (Cyber-Physical Systems
Week) to be held in Seattle, USA, collocating 5 conferences: HSCC,
the International Conference on Cyber-Physical Systems (ICCPS),
the International Conference on Information Processing in Sensor Networks
(IPSN), the Conference on High Confidence Networked Systems (HiCoNS), and
the Real-Time and Embedded Technology and Applications Symposium (RTAS).
Special Issue: Authors of distinguished papers will be invited to
submit an extended version of their work for possible publication in a
special issue of the journal Nonlinear Analysis: Hybrid Systems.
Best Student Paper Award: As established in the previous years, a best
student paper award will be given to a contribution which has been
primarily authored by a student. Each paper nominated for this award
should be co-authored primarily by a student (as certified by the
student’s faculty advisor).
Repeatability Evaluation: HSCC has a history of publishing strong
papers emphasizing computational contributions; however, recreating
these computational elements is hard, because details of the
implementation are unavoidably absent in the paper. Following a
successful inaugural run in 2014, authors of papers accepted to HSCC
(in any track) that contain a computational component will be invited
to participate in an optional repeatability evaluation process after
final submission of the paper in February. Papers that pass will be
highlighted at the conference, and all submissions will receive
confidential feedback from independent reviewers on any challenges faced
in recreating the computational results. Review criteria and
suggestions on how to get started on reproducible research are posted
at the conference web page (http://2015.hscc-conference.org).
Submission Guidelines
Submitted papers should present original research that is unpublished and not
submitted elsewhere.
Regular papers: maximum 10 pages in the 10pt, two-column ACM format.
Submission by October 20, 2014 through the EasyChair system. Regular
papers should present original research or industrial applications of
techniques for design and/or analysis of hybrid systems, or their
integration into industrial design flows.
Tool and Case-Study papers: maximum 6 pages in the 10pt, two-column
ACM format. Submission by October 20, 2014 through the EasyChair
system. Tool Papers should describe an implemented tool and its novel
features. Case studies should present hybrid systems tools or
techniques.
Submissions of Regular, Tool and Case-Study papers should be made
through the HSCC 2015 EasyChair submission website:
https://www.easychair.org/conferences/?conf=hscc2015
Demo/poster abstracts: Approximately 2 pages. Submission by January
10, 2015 through email to hscc2015(a)easychair.org with “HSCC demo/poster
submission” in the subject line. Questions should be directed to the
same address. Demo/poster abstracts serve the sole purpose of
selecting contributions for the demo and poster session and will not
be published in the conference proceedings.
Program Chairs
Antoine Girard, University of Grenoble, France.
Sriram Sankaranarayanan, University of Colorado, Boulder, USA.
Publicity Chair
Sayan Mitra, University of Illinois, Urbana-Champaign, USA.
Repeatability Evaluation Chair
Ian Mitchell, University of British Columbia, Vancouver, Canada.
Program Committee
Erika Abraham, RWTH Aachen University, Germany
Matthias Althoff , TU Ilmenau, Germany
Shun-ichi Azuma, Kyoto University, Japan
Hamsa Balakrishnan, MIT, USA
Mireille Broucke, University of Toronto, Canada
Krishnendu Chatterjee , IST Austria, Austria
Thao Dang, VERIMAG, France
Jyotirmoy Deshmukh, Toyota Motors, USA
Alexandre Donzé , UC Berkeley, USA
Georgios Fainekos, Arizona State University, USA
Eric Feron, Georgia Institute of Technology, USA
Martin Fränzle, Carl von Ossietzky Universität Oldenburg, Germany
Eric Goubault, CEA France and Ecole Polytechnique, France
Radu Grosu, Vienna University of Technology, Austria
Maurice Heemels, TU Eindhoven, Netherlands
Jun-ichi Imura, Tokyo Institute of Technology, Japan
(Samuel) Qing-Shan Jia, Tsinghua University, PR China
Marta Kwiatkowska, Oxford University, England
Kim Larsen, Aalborg University, Denmark
Javad Lavaei, Columbia University, USA
John Lygeros, ETH Zurich, Switzerland
Sayan Mitra, University of Illinois at Urbana Champaign, USA
Jens Oehlerking , Robert Bosch GmbH, Germany
Meeko Oishi, University of New Mexico, USA
Necmiye Ozay, University of Michigan, USA
Carla Piazza, University of Udine, Italy
Andre Platzer , Carnegie Mellon University, USA
Pavithra Prabhakar, IMDEA Software Institute, Spain
Maria Prandini, Politecnico di Milano, Italy
Daniel Quevedo, University of Newcastle, Australia
Jörg Raisch, TU Berlin, Germany
S Ramesh, General Motors, USA
Kohei Suenaga, Kyoto University, Japan
Danielle Tarraf, Johns Hopkins University, USA
P.S. Thiagarajan, National University of Singapore, Singapore
Ufuk Topcu, University of Pennsylvania, USA
Ashuthosh Trivedi, IIT Bombay, India
Jana Tumova, KTH, Sweden
Majid Zamani, Technical University of Munich, Germany
Naijun Zhan, Chinese Academy of Sciences, PR China\
Steering Committee
Rajeev Alur, University of Pennsylvania, USA
Bruce Krogh, Carnegie-Mellon University, USA
Oded Maler, Verimag, France
Claire Tomlin, University of California Berkeley, USA
Werner Damm, OFFIS, Germany
--
Kohei Suenaga (末永幸平), Ph.D
Associate professor (准教授)
Graduate School of Informatics, Kyoto University
(京都大学情報学研究科)
ksuenaga(a)gmail.com
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/
[View Less]
Prof. Aleksy Schubert at NII Logic Seminar
Date: September 26, 2014, 14:00--16:00
Place: National Institute of Informatics, Room 1716 (17th floor)
場所: 国立情報学研究所 17階 1716室
(半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
(地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Aleksy Schubert (University of Warsaw)
(1)
Title: Undecidability and complexity in fragments of first-order
intuitionistic logic
Abstract:
In case of classical first-order logic there is a full
characterisation of …
[View More]decidable and undecidable classes of formulae
depending on the quantifier prefix and the vocabulary that is
used. First-order logic in intuitionistic case lacks this kind of
classification since there is no prefix normal form and actually the
prenex fragment of the logic is in many cases much weaker than the
general calculus. However, there is one meaningful stratification of
the intuitionistic logic similar to the prenex form. We can consider
classes of formulae that would result in a particular prefix of
quantifiers when transformed using classical equivalences. The status
of decidable and undecidable cases within this stratification will be
presented as well as the complexity of known subcases.
(2)
Title: Verification of programs using Frama-C and Why3
Abstract:
Frama-C is a tool that makes it possible to do a variety of analyses
for C programs annotated with C specification language called ACSL
(The ANSI/ISO C Specification Langage). One of the possible ways to
use Frama-C is to generate verification conditions for appropriately
defined Hoare logic that is in line with C programming language
semantics. These verification conditions can subsequently be
discharged by Why3 tool that makes it possible to manage the proving
of necessary properties. During the talk I will present an overview of
the tools and show a number of interesting examples to demonstrate how
these tools work together to make possible verification of practical
programs.
問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta(a)nii.ac.jp
http://research.nii.ac.jp/~tatsuta
[View Less]
九州大学マス・フォア・インダストリ研究所の溝口先生の代理で投稿いたします.
=========================================================================
研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
(English version is below.)
12月3日(水)-5日(金)に九州大学西新プラザにて,
研究集会「高信頼な理論と実装のための定理証明および定理証明器」
を開催します. 皆様のご参加をお待ちしています.
日時:2014年 12月3日(水) 〜 12月5日(金)
場所:九州大学・西新プラザ
(福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin
福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分.
プログラム:
詳細は未定(準備中)です. みなさまのご講演をお待ちしています.
Adam Chlipala氏 (MIT, USA), …
[View More]Cyril Cohen 氏 (Univ. Gothenburg,
Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する
御講演を頂く予定です.
参加者と講演の数を大体把握しておきたいと思いますので,参加される方は
10月半ばまでに下の参加申し込みを下記メールアドレスまでお送りください.
参加者には,できるだけ講演していただければと思います.
申込み・問い合わせ先:
tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学))
URL: http://coop-math.ism.ac.jp/event/2014E04
(注. 作成途中です.「TPP2014 数学」で検索してみて下さい.)
-------------------------------------------------------------------------
TPP 2014 参加申し込み
お名前:
ご所属:
講演 :する/しない
懇親会:参加する/参加しない
講演する場合
タイトル:
(講演のタイトルが決まっていなければ,TBAでもかまいません.
決まったらご連絡ください.)
講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5
その他(ご意見/ご要望ありましたらお願いします):
-------------------------------------------------------------------------
=========================================================================
Workshop:
Theorem proving and provers for reliable theory and implementations (TPP2014)
This is the call for participation for TPP2014,
to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University.
Date: 2014/12/03 around 1pm to 12/05 around 3pm
Venue: Nishijin Plaza, Kyushu University
(2-16-23 Nishijin, Sawara-ku, Fukuoka City)
http://bit.ly/QdaiNishijinPDF
Invited Speakers:
Adam Chlipala (MIT, USA)
Cyril Cohen (Univ. Gothenburg, Sweden)
If you are planning to attend the meeting, please send the information
slip below to the indicated address by mid-October.
Submission/questions to:
tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi)
URL: http://coop-math.ism.ac.jp/event/2014E04
(Tentative Japanese HP. Revised English HP will be notified later.)
-------------------------------------------------------------------------
TPP 2014 Registration
Name:
Affiliation:
Will give a talk: Yes/No
Will attend the party: Yes/No
Title of the talk: (If it is not decided yet, TBA is OK.)
Which date do you prefer to talk ?
12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG)
Requests for the organizer (if any):
-------------------------------------------------------------------------
=========================================================================
[View Less]
Prof. Aart Middeldorp at NII Logic Seminar
Date: September 22, 2014, 14:00--16:00
Place: National Institute of Informatics, Room 2005 (20th floor)
場所: 国立情報学研究所 20階 2005室
(半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
(地図 http://www.nii.ac.jp/about/access/)
Speaker: Prof. Aart Middeldorp (University of Innsbruck)
Title: Proving AC Termination by Knuth-Bendix Orders
Abstract:
Equational theories that contain axioms expressing associativity and
commutativity (AC) of certain operators are …
[View More]ubiquitous. Theorem proving
methods in such theories rely on well-founded orders that are compatible
with the AC axioms. In this talk we consider various definitions of
AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin
and Voronkov are revisited. The former is enhanced to a more powerful
AC-compatible order and we modify the latter to amend its lack of
monotonicity on non-ground terms. We present new complexity results and
compare the various orders on problems in termination and completion.
The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and
Akihisa Yamada.
問合せ先:
龍田 真 (国立情報学研究所)
e-mail: tatsuta(a)nii.ac.jp
http://research.nii.ac.jp/~tatsuta
[View Less]
皆様、
FAU Erlangen-Nürnberg の Tadeusz Litak さんの講演のお知らせです。
ふるってご参加ください。
問い合わせ先:
佐野勝彦
北陸先端科学技術大学院大学 情報科学研究科
e-mail: v-sano(a)jaist.ac.jp
----------------------------------------------------------------------------------------------------
* JAIST Logic Seminar Series *
Date: Thursday, 18th September, 2014, 15:10-17:00
Place: JAIST Collaboration Room 6 (I57-g)
(Access:http://www.jaist.ac.jp/english/location/access.html)
Speaker: Tadeusz Litak (Department Informatik, Technische Fakultät,
FAU …
[View More]Erlangen-Nürnberg, Germany)
Title: Relational lattices
Abstract:
We study an interpretation of lattice connectives as natural join and
inner union between database relations with non-uniform headers. We
show that this interpretation proposed by database experts (Vadim
Tropashko from Oracle) yields a class of lattices which has not been
considered in the existing lattice-theoretical literature. We discuss
axiomatizability and decidability of their (quasi-)equational theory
and propose an equational axiomatization for a corresponding abstract
algebraic class. It turns out that addition of just the “header
constant” to the lattice signature already allows mimicking the Maddux
technique for cylindric algebras and encode the word problem for
semigroups in the quasiequational theory. Relational lattices,
however, are not as intangible as one may fear: for example, they do
form a pseudoelementary class. We also apply the tools of Formal
Concept Analysis and investigate standard contexts of relational
lattices, obtaining, e.g., results on their subdirect irreducibility.
This is a joint work with Szabolcs Mikulas and Jan Hidders
----------------------------------------------------------------------------------------------------
[View Less]