 |
24 elements available | | POSTDOC IN CONSTRAINTS AND OPTIMIZATION, DL 28 FEB 2013 3:00 PM EET
The Finnish Center of Excellence in Computational Inference Research
(COIN), a joint research center of Aalto University and University of
Helsinki, is now seeking a Postdoctoral researcher in Constraints and
Optimization to work in the Computational Logic Group, led
by professor Ilkka Niemela and co-led by professor Tomi Janhunen, and
with opportunities for collaboration with other professors of COIN.
Candidates having a strong background in constraint and rule based
modeling (e.g. answer set programming, constraint satisfaction,
propositional satisfiability and its extensions) and optimization
techniques are encouraged to apply. Experience in the development of
reasoning algorithms and solvers and, in particular, in their
implementation on parallel architectures (multi-core CPUs, clusters,
grids), is considered as an asset.
The Finnish Center of Excellence in Computational Inference Research
(COIN) works on fundamental questions of inference and in applications
in Intelligent Information Access, Computational Molecular Biology and
Medicine, Computational History, Computational Climate, Computational
Neuroscience and other directions yet to be determined.
More information:
COIN,
Aalto University,
University of Helsinki. |
| |  | |  |
| | |
| |
One post-doc position in ICT on the research project
"Advanced SMT Techniques for Word-level Formal Verification - (WOLF)"
is available in Trento, Italy, under the joint supervision of
- Alessandro Cimatti, FBK, Trento, and
- Roberto Sebastiani, DISI, University of Trento.
The research activity will be carried out jointly within the Embedded
Systems (ES) Research Unit of the Center for Scientific and
Technological Research of the Fondazione Bruno Kessler (FBK), Trento,
and the Software Engineering, Formal Methods & Security Research
Program, at Department of Information Engineering and Computer Science
(DISI) of University of Trento.
Aim and Scope
=============
The research activity will aim at investigating and developing novel
techniques, methodologies and support tools for Satisfiability Modulo
Theories (SMT) for the formal verification of systems. This work will
be part of the "Advanced SMT Techniques for Word-level Formal
Verification - (WOLF)" project, a three-year research project
supported by SRC/GRC (http://www.src.org/compete/s201113/), in strict
collaboration with the Formal Verification Group at Intel, Haifa, and
other major HW companies.
The ultimate goal of the WOLF project is to provide a comprehensive
SMT package to support effective formal verification of systems
ranging from RTL circuits all the way up to high-level hardware
description languages (e.g. SystemC) and software. The package will be
implemented on top of the MathSAT SMT platform
(http://mathsat.fbk.eu/), and provided as an API.
Candidate Profile
=================
The ideal candidate should have an PhD in computer science or related
discipline, and combine solid theoretical background and excellent
software development skills (in particular C/C++).
A solid background knowledge and/or previous experience on one of the
following topics (in order of preference) is required:
Satisfiability Modulo Theory (SMT), Propositional Satisfiability (SAT),
Model Checking, Automated Reasoning.
Previous experience in the following areas will also be considered
favourably: Constraint Solving and Optimization, Embedded Systems
Design Languages (e.g. Verilog, VHDL).
The candidate should be able to work in a collaborative environment,
with a strong committment to reaching research excellence and achieving
assigned objectives.
Terms and dates
===============
The position will start as soon as possible, and will have to be
renewed yearly, for a maximum of two years. The expected salary
will range from about 2200 to 2400 euros net income, and the gross
will include previdential (social security) contributions. Facilities
for meals at the local canteen can be provided.
Applications and Inquiries
==========================
Interested candidates should inquire for further information and/or
apply by sending email to wolf-recruit@disi.unitn.it, with subject
'POSTDOC ON WOLF PROJECT'.
Applications should contain a statement of interest, with a Curriculum
Vitae, and the names of reference persons. PDF format is strongly
encouraged. It should also indicate an estimated starting date.
Contact Persons
===============
Dr. ALESSANDRO CIMATTI,
Embedded Systems Research Unit,
FBK-Irst,
via Sommarive 18, I-38123 Povo, Trento, Italy
http://sra.fbk.eu/people/cimatti/,
Prof. ROBERTO SEBASTIANI
Software Engineering, Formal Methods & Security Research Program
DISI, University of Trento,
via Sommarive 14, I-38123 Povo, Trento, Italy
http://disi.unitn.it/~rseba/.
|
| | | | |
| | |
|  | |  | | | | | Date: | 17-Jan-2013 | | Title: | Internship Position at IBM Research, AI for Optimization group
| | Hits: | 248 | | Contributed by: | Ashish Sabharwal | | Keywords: | Local Search, SAT application, Learning, SAT tools, Distributed Computing, CSP, Linear Programming, pseudo boolean optimization, Genetic Algorithm, New research position, Satisfiability Modulo Theory, Constraint Programming, Job, SAT/CP Integration, null, null, null, null, null, null, null |
| | | |  |  | |
| | A summer internship position is available for 2013 in the "AI for Optimization" group within the Business Analytics and Mathematical Sciences department at IBM Watson Research Center, Yorktown Heights, New York. The internship will last for about 3 months and will be scheduled between March and October, 2013.
Candidates should be exceptional Masters or PhD students in Computer Science and related areas, and not have already received their PhD by the internship start date. The successful candidate is expected to have strong interest and some experience in one or more of the following:
- Developing Novel Technologies based on AI and OR to advance the state of the art in combinatorial optimization (e.g., Heuristic Search, Mixed Integer Programming (MIP), Linear Programming (LP), Satisfiability (SAT))
- Robust Parallelization of search-based algorithms (e.g., using parallel Branch&Bound; information exchange) exploiting novel computing architectures such as BlueGene, multi-core end-user machines, large compute clusters, and the Cloud
- Advancing Simulation-Based Optimization approaches to solve real-world problems and/or to improve optimization methods themselves by, e.g., employing techniques from Machine Learning, Local Search, and Genetic Algorithms for automated algorithm selection and parameter tuning
- Applications of Optimization to Analytics, Production Modeling, Sustainability, Systems, and Databases
Interested candidates should send their CV as well as names and contact information of at least two references to all of the following:
Ashish Sabharwal [ashish.sabharwal@us.ibm.com]
Horst Samulowitz [samulowitz@us.ibm.com]
Meinolf Sellmann [meinolf@us.ibm.com] |
| | | | |
| | |
| |
Description:
============
Two post-doctoral research positions available at INESC-ID. The
post-doctoral researchers will conduct research work in Boolean-based
decision procedures, including algorithms for Boolean Satisfiability,
Quantified Boolean Formulas (QBF) and Boolean Optimization. Examples
of research include new algorithms for QBF, Maximum Satisfiability,
Minimal Unsatisfiability and practical applications.
Requirements:
=============
Applicants should have a PhD degree in Computer Science or related
area, be fluent in English, have a strong publication record and show
evidence of autonomous research ability. Successful candidates will be
integrated in the SAT group at INESC-ID to work on algorithms and
tools for constraint solving.
Additional Information:
=======================
The post-doctoral researcher positions are funded by the national
research grants ATTEST and POLARIS. More information is available from:
http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=32273
and,
http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=32274
|
| | | | |
| | |
| |
The Software Design Group in MIT’s Computer Science and Artificial Intelligence Lab (CSAIL) is hiring a Research Scientist to participate in research and development of the Alloy language and analyzer.
Alloy (http://alloy.mit.edu) is a lightweight modeling language with an automatic analyzer based on SAT. It has been used in a wide range of applications in software engineering, including the design of access control schemes, security mechanisms, network protocols, ontologies, and so on. In addition to design analysis, Alloy has also been used for code verification, test case generation and automatic configuration. Alloy was introduced in 1997, and is now in version 4. Hundreds of papers have been written describing research based on Alloy; for examples, see http://alloy.mit.edu/applications.html. Alloy has also been taught in dozens of university courses.
Our plan now is to take Alloy in new directions, and dramatically improve the usability and scalability of the analyzer. We are looking for someone who is is excited by these possibilities and will be deeply involved not only in design and implementation but also in strategic planning. There are also opportunities to co-advise students and participate in research proposals.
Qualifications should include:
- a PhD in computer science or a related field;
- superb programming skills, preferably with experience of writing compiler-like tools;
- familiarity with logic and model checking;
- a passion for design;
- excellent communication and writing skills;
- ability to work both independently and cooperatively with others.
Please apply online to MIT (http://jobs.mit.edu/) with resume and cover letter, and include the following in your application (sent separately to djresci@csail.mit.edu): (A) A list of languages and technologies you're familiar with; (B) A short sample of something you've written in English, and a small code sample; (C) A short answer to the question: "If you could make one big change to the Alloy system, what would it be?" Please reference MIT job number 00008292 in your application.
|
| | | | |
| | |
| | A postdoctoral position is available in research project ATTEST: AlgoriThms and Tools for reasoning about dEpendable SysTems. The position is available for 1 year, starting on January 1st, 2012, and may be eventually renewed.
Applications are welcome until November 26th.
More details can be found here. |
| | | | |
| | |
| | A summer internship position is available for 2012 in the "AI for
Optimization" group at IBM Watson Research Center, Yorktown Heights, New York.
The internship will last for about 3 months and will be scheduled between March
and October, 2012.
Candidates should be exceptional Masters or PhD
students in Computer Science and related areas, and not have already received
their PhD by the internship start date.
The successful candidate is
expected to have strong interest and some experience in one or more of the
following:
- Developing novel technologies based on AI and OR to advance the state of the
art in combinatorial optimization (e.g., Heuristic Search, Mixed Integer
Programming (MIP), Linear Programming (LP))
- Robust parallelization of search-based algorithms (e.g., using parallel
Branch&Bound; information exchange) exploiting novel computing architectures
such as BlueGene, multi-core end-user machines, large compute! clusters, and the
Cloud
- Advancing simulation-based optimization approaches to solve real-world
problems and to improve optimization methods themselves by, e.g., employing
techniques from Machine Learning, Local Search, and Genetic Algorithms for
automated algorithm selection and parameter tuning
- Applications of Optimization to Analytics, Production Modeling,
Sustainability, Systems, and Databases
Due to strict time
constraints, interested candidates should immediately contact us with
their CV as well as names and contact information of at least two
references.
Ashish Sabharwal [ashish.sabharwal@us.ibm.com]
Horst
Samulowitz [samulowitz@us.ibm.com]
Meinolf Sellmann
[meinolf@us.ibm.com]
|
| | | | |
| | |
| | Title
-----
Innovative approaches to guarantee correctness while designing embedded systems
Location
-----------
Group of Computer Architecture headed by Prof. Dr. Rolf Drechsler
University of Bremen, Bremen, Germany
Application
---------------
The deadline for applications is July 10th 2011. Applications including CV, certificates, and recommendation letters should be sent by email to Rolf Drechsler (drechsle@uni-bremen.de). Please refer to reference number A 93/11.
Salary
-------
Dependent on the qualification of the applicant the salary grade for the position as a researcher (Wissenschaftliche/r MitarbeiterIn) will be TVL 13 or TVL 14, i.e. net income per month around 1800 EUR or 2000 EUR, respectively. The project will start on August 1st 2011.
Abstract
----------
The internationally renowned Group of Computer Architecture at the University of Bremen develops design automation tools for circuits and systems. Focus of the offered position will be the development of innovative approaches to guarantee correctness while designing embedded systems. The position is part of a research project funded by the German Research Foundation (DFG) for 5 years within a Reinhart Koselleck-Project.
The research group tightly cooperates with industrial partners within transfer projects, funded e.g. by the German Ministry for Education and Research (BMBF). Within the Graduate School of Embedded Systems (GESy) at the University of Bremen, new methods and techniques are developed and evaluated in real-world settings. Tight interaction of the applicant with these projects is expected.
Requirements
• Diploma or Master Degree with at least 300 CP in computer science or related subject
• Profound knowledge of formal methods
• Excellent programming skills in C/C++
• Strong scientific interest and willingness to cooperate with other projects and researchers
Further Information
----------------------------
For further more detailed information please refer to the official announcement (in German)
http://www.uni-bremen.de
also consider
http://www.uni-bremen.de/
or directly contact:
Prof. Dr. Rolf Drechsler
Group of Computer Architecture, Department 3, University of Bremen, Germany
Phone: +49-421-218-63932
Email: drechsle@uni-bremen.de
|
| | | | |
| | |
| |
PhD / PostDoc Position Opening
The research group "Verification meets Algorithm Engineering" at the
University of Karlsruhe is offering a PhD/PostDoc position in the
area of software verification and SAT solving.
The focus of this position is on software verification using bounded model
checking, new algorithms for SAT solving and SMT (satisfiability modulo theory).
Applicants should have a solid theoretical background in formal methods
or mathematical logic, as well as outstanding programming skills.
Interest in applications of SAT solving, software verification (especially
bounded model checking), and compiler technology is appreciated.
The position is initially available for up to three years (with a possible
extension) and is open immediately.
For additional information or to apply for this position send an e-mail with
the usual documents to sinz@ira.uka.de.
Carsten Sinz
TU Karlsruhe
|
| | | | |
| | |
| |
Dear all,
Microsoft Research Cambridge is opening a three-month
internship position on parallel SAT. The main work location is Cambridge (UK),
but the candidate will have to travel to Redmond (US) at the beginning of her
internship. The objective of the work is to study and implement innovative
parallel search techniques.
Required skills: C++, C#.
Optional skills: Windows threads, MPI, knowledge of
classical parallel search techniques.
Agenda: asap.
Thanks for forwarding to interested parties.
|
| | | | |
| | |
| | | | | | | | Date: | 23-Apr-2008 | | Title: | Doctoral Student Positions Available
| | Hits: | 915 | | Contributed by: | | | | | | | | | Date: | 23-Apr-2008 | | Title: | Post-Doc Positions Available
| | Hits: | 945 | | Contributed by: | | |
Prover Technology develops formal verification technology for the proof engine product line Prover
Plug-In. This product line includes proof engines both for combinational logic and for sequential
logic, and various high-level data types. Prover Plug-In products are used in company-internal tools
but are also licensed to tool vendors for formal verification tasks involving model checking,
equivalence checking, formal verification and automatic test case generation.
Applicants should preferably have a M.Sc. or Ph.D. in Computer Science or Mathematics with a minimum
of two years of programming (C/C++) experience. A suitable candidate is expected to have good
communication skills, be fluent in English, and proven experience in developing low-level formal
verification algorithms using SAT or BDD technologies. Additional experience from relevant areas is
a plus. Highly motivated and academically strong applicants interested in getting into the field are
also encouraged to apply.
Requirements:
· PhD or M.Sc. in Computer Science, Mathematics or a related field with a minimum of two years of
programming (C/C++) experience. Exceptional candidates with BS or recent graduates with significant
experience and skills listed below will also be considered.
· Excellent communication and problem solving skills.
AND one or more of the following:
· Very strong programming skills with experience in developing advanced algorithms in C/C++
· Experience with SAT, binary decision diagrams (BDDs), model checking and related applications thereof
· Two years of experience in development of formal verification technology and tools
If you are interested please email an application (including resume, references, sample papers, and
statement of research and development interests) to jobs@prover.com.
|
| | | | |
| | |
| |
Sr. Developer
Requirements
1. Back ground and strong interest in developing an EDA product/s:
tools based on Verilog, Vera and SystemVerilog Hardware Description Languages.
2. Very good technical expertise in formal area: SAT solvers, BDD techniques,
symbolic simulation, equivalence checkers, model checking,
constraint solver, sequential equivalence checker, etc.
3. Capable of research, but is hands on and able to break an algorithm
into projects as a technical lead.
4. Experience in managing a small team is a plus, but not a must.
Experience in doing research is a plus, but not a requirement.
Steve Pace
Sr. Recruiter
Nusym Technology
space@nusym.com
www.nusym.com
|
| | | | |
| | |
| | [Apologies for multiple copies]
The Constraint Reasoning Group of Microsoft Research Cambridge is opening a two-year post-doctoral position in Cambridge, UK. Current CRG research efforts are related to stochastic optimization, SAT/SMT/CP Integration, automated parameter tuning, etc. The group is applying its research to a very large scope of applications: software verification, business processes, planning and scheduling, graphics, etc. The successful candidate will pursue fundamental research in constraint reasoning. She or he will also be involved with engineers and architects from Microsoft product groups. This will give to the candidate an unique opportunity to pursue fundamental research while being exposed to long term industrial challenges.
Ideally, the candidate should have strong skills in combinatorial search, constraint programming, SAT. Knowledge in machine learning, probabilistic reasoning, stochastic local search, or control theory is a plus. A general AI background would be also very appreciated. Technically, the ideal candidate will have a deep knowledge in C# and C++.
Requirements: Candidates must have completed their PhD by July 2007.
Expected start: July-December 2007.
Interested candidates should send a cover letter including personal and scientific CV, list of publications and names of three references to Youssef Hamadi ( youssefh at microsoft dot com ) . In addition, candidates will have to register themselves through the following link http://research.microsoft.com/aboutmsr/labs/cambridge/postdoc.aspx.
Youssef |
| | | | |
| | |
| | | Post-Doctoral positions are available for work on the
MX Project
at Simon Fraser University. Applicants should contact
project leaders by February 10, 2007. |
| | | | |
| | |
| | | | | | | | Date: | 13-Dec-2006 | | Title: | Post-Doctoral Positions
| | Hits: | 1291 | | Contributed by: | | |
Doctoral Student positions at the University of Genoa - Italy
=============================================================
The Laboratory of Systems and Technologies for Automated Reasoning
(http://www.star-lab.it/) at the University of Genoa is looking for Doctoral
students in the following disciplines:
1. Automated Reasoning, Formal Verification and Planning: The main task is
to
continue the development of our tool QuBE, a state-of-the-art
solver for Quantified Boolean Formulas (see
http://www.qbflib.org). The overall goal is to make it successfully
applicable to formal property verification and automated planning
reasoning tasks. In this context, STAR-Lab organizes the QBF
solvers competition (formerly comparative evaluation) and maintains
the site www.qbflib.org. Candidates wishing to help also in such tasks
are welcome. Specific skills required: some knowledge of
propositional logic and/or of formal verification are a plus.
2. Software Testing: The main task is to assess the state-of-the-art
in currently applied methodologies and tools for software testing
in industry. Goal of the thesis is the definition of new
methodologies and/or support tools for software testing aiming to
improving the overall productivity of the software production
life-cycle. This position is sponsored by a leading industry in
Genova and the candidates are required to maintain a very strict
collaboration between the research groups in the university and in
the industry. Specific skills required: some knowledge of
software testing methodologies and support tools are a plus.
3. Biomedical Informatics: The main task is to do research towards a
doctoral Thesis on Biomedical Informatics, an emergent discipline
at the crossroads between Bioinformatics and traditional Medical
Informatics. The main topic of the thesis will be advanced Semantic
Integration, i.e., merging etherogeneous and possibly unstructured
information sources to enable efficient knowledge represenation
(ontologies) and discovery (data mining). The developed algorithms
will be employed in the context of Service Oriented Architectures
(S.O.A., e.g., Web Services) leveraging geographically distributed
computing resources (e.g., GRID). Specific skills required: a
sufficient knowledge of basic S.O.A. enabling technologies, like
client/Server architectures, SOAP, WSDL, XML, are a plus.
The positions are part of various projects funded by the Italian Government
and the European Union. The tentative start date of the posts is 1st of
January 2007, and the posts have currently granted funding until the end of
2009, subject to annual evaluations. The posts will be granted after a
successfull trial period of 2/3 months, during which the perspective
applicants will be supported by existing grants and have a chance to
familiarize with our staff and work on the same topics of the PhD Thesis.
The ideal applicant should hold a Master's degree in computer science or
related field. Beside the specific skills required by the specific calls,
the ideal candidate should have good knowledge in Software Engineering,
Artificial Intelligence, Knowledge Based Reasoning, or otherwise related
topic, and should have good programming skills. The international applicant
should also have very good English language skills as demonstrated by an
TOEFL IELTS, or Cambridge Language Certificate (CAE/CPE) score, or
equivalent.
The applications with a letter of introduction containing contact
information for two persons willing to act as a reference, CV, and official
copies of the relevant diplomas should arrive before September 30, 2006 at
the address:
Enrico Giunchiglia
DIST - Viale Causa 15
16145 Genova
Italy
For enquiries contact:
Enrico Giunchiglia
enrico@dist.unige.it
(http://www.star-lab.it/~enrico/)
Armando Tacchella
tac@dist.unige.it
(http://www.star-lab.it/~tac/)
|
| | | | |
| | |
© 2000-2001 Business & Technology Research Laboratory.
© 2001-2005 Centre de Recherche en Informatique de Lens.
Hosted by Innovation
and Technology Research Lab.
Please send any comment to daniel@satlive.org.
|
|
|
|
|
|
|
|
|
|
| |
