| Legal
Status |
|
Permanent
resident of the United States (green card holder), Russian citizen |
| |
|
|
| Education |
|
The
Graduate Center of the City University of New YorkNew York, NY |
| 2001-2005 |
|
Ph.D. in Computer Science |
| |
|
|
| |
|
Moscow
State UniversityMoscow, Russia |
| 1993-1998
|
|
Diploma
with honours (M.Sc. in Mathematics),
Department of Mechanics and Mathematics, Division of Mathematics, major
- Mathematics and Applied Mathematics |
| 1994-1996
|
|
Computer
Academy, Moscow State UniversityMoscow, Russia |
| |
|
|
| Research
Interests |
|
Software
reliability, testing and verification. Systems for computer-aided
formal reasoning, higher-order theorem provers and logical frameworks.
Automatic proof search. |
| |
|
|
| Research |
|
|
| Experience
|
|
CAISS, City College of New York, NY
|
| Since Jan 2006 |
|
Research Associate |
|
|
Development of Caiss-Stat - a statistical package
which is much easier to learn and use
than other mainstream packages (Statistica, SPSS, JMP6, etc).
|
|
|
Connecting Caiss-Stat to open-source R statistical package.
|
|
|
Work on Magnus computational algebra package.
|
|
|
Cryptographic uses of Magnus.
|
|
|
Development of a non-hierarchical tag-cloud based file system
which is transparent to legacy software and
uses a transparent embedding into a regular file system
for file storage.
|
|
|
|
|
|
California
Institute of TechnologyPasadena, CA |
| Jun-Jul
2005 |
|
Visitor
with Prof. Jason Hickey. |
| |
|
Revised
Jprover, the automatic prover for first-order intuitionistic logic, a
part of the MetaPRL system. |
| |
|
Made
substantial speed improvements, added support for modal logic. |
| |
|
Devised
and implemented support for the logic with justified common knowledge. |
| |
|
Devised
and implemented a standalone tableau-based prover for logic of proofs. |
| |
|
|
| |
|
Microsoft
ResearchRedmond, WA |
| Jun-Sep
2002 |
|
Intern
with Wolfram Schulte, Foundations of Software Engineering group. |
| |
|
Developed
a tool for automated test case generation for a given executable
http://www.research.microsoft.com/fse/AsmL/AsmL-specification.
The test case generation was based on run-time information about path
coverage in a specification. |
| |
|
|
| |
|
Moscow
State UniversityMoscow, Russia |
| 1995-2001
|
|
Department
of Mathematical Logic and Theory of Algorithms, Laboratory for Logical
Problems in Computer Science. Advisors: Prof. Sergei Artemov, Assistant
Prof. Vladimir Krupski. |
| 1998-2001
|
|
Efficiency
improvements in MetaPRL. |
| May
1998 |
|
Diploma
Thesis: Theory of Random Access Memory in NuPRL. |
| 1995-1997
|
|
Participated
in the development of compiler test suite for C++ standard compliance,
under Prof. Vladimir Sukhomlin. |
| |
|
|
| |
|
Open
Mining Research InstituteChelyabinsk, Russia |
| 1993
|
|
Developed
modelling software for minimizing movement of waste rock in excavations
(with Valeriy Nechunaev). The work was done by a contract with open-pit
mine ``Borodinskiy'', Krasnoyarsk, Russia. |
| Teaching |
|
|
| Experience |
|
Graduate
Center of the City Univercity of New YorkNew York, NY |
| Spring
2005 |
|
TA,
graduate CS course ``Logical Foundations of Artificial Intelligence'' |
| |
|
|
| |
|
City
College of the City University of New YorkNew York, NY |
| Spring
2005 |
|
TA,
undergraduate CS course ``Programming Language Paradigms'' |
| Fall
2003 |
|
Instructor,
undergraduate CS course "Introduction to Programming and Computer
Science" |
| Summer
2003 |
|
Instructor,
undergraduate CS course "Algorithms" |
| Spring
2003 |
|
Instructor,
undergraduate Math course "Calculus I" |
| |
|
|
| Work |
|
|
| Experience |
|
New
York City College of Technology, CUNYNew York, NY |
| 2002-2003
|
|
Self
Regulatory Learning Project: |
| |
|
Developed
a system for self-evaluation of learning progress, plaforms: PocketPC
and Microsoft Outlook. |
| |
|
|
| |
|
http://www.trustlink.comTrustLinkMoscow,
Russia/Stockholm, Sweden |
| 2000-2001
|
|
Software
Analyst:
Designed and implemented data-synchronization subsystems for several
projects, spanning
PalmOS, EPOC, PocketPC and PC platforms. |
| |
|
I
was actually hired as a Junior Developer but in a few months received a
promotion to Analyst position. |
| |
|
|
| |
|
Family
businessChelyabinsk, Russia |
| 1991-1998
|
|
Lead
Developer: Developed a number of accounting systems for
small-sized companies (with my father). This family business was and
remains so far the main source of income for my parents. |
| |
|
|
| Publications |
|
|
|
|
Gilber Baumslag, Yegor Brukhov, Benjamin Fine,Gerhard Rosenberger.
Encryption methods using formal power series rings.
Prepublicacions del Centre de Recerca Matemàtica; 725 2006/2007
|
|
|
|
|
|
Yegor Bryukhov. Integration of Decision Procedures into High-Order Interactive Provers. PhD Thesis. The Graduate Center of the City University of New York, 2006. |
|
|
|
| |
|
Yegor
Bryukhov.
Automatic Proof Search in Logic of Justified Common Knowledge. Accepted
to the 4th Methods for Modalities Workshop (M4M'05). |
| |
|
|
| |
|
Natalia
Novak and Yegor Bryukhov.
Implementing the Calculus of Inductive Constructions in the MetaPRL
framework.
In Konrad Slind, editor, 17th International Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2004).
Emerging Trends Proceedings,
pages 153-164. University of Utah, 2004. |
| |
|
|
| |
|
Yegor
Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin.
Implementing and Automating Basic Number Theory in MetaPRL Proof
Assistant. In David Basin and Burkhart Wolff, editors,
16th
International Conference on theorem Proving in Higher Order Logics
(TPHOLs 2003).
Emerging Trends Proceedings,
pages 29-39. Universität Freiburg, 2003. |
| |
|
|
| |
|
Jason
Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli
Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov,
Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt,
Carl Witty, and Xin Yu. MetaPRL -- A Modular Logical Environment.
In David Basin and Burkhart Wolff, editors,
Proceedings of the 16th International Conference on
Theorem Proving in Higher Order Logics
(TPHOLs 2003), volume 2758 of Lecture Notes in
Computer Science, pages 287-303. Springer-Verlag, 2003. |
| |
|
|
| Online |
|
|
| Publications |
|
Jason
Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin,
and Xin Yu. A listing of MetaPRL theories.
http://metaprl.org/theories.pdf |
| Awards |
|
|
| 1993
|
|
Russian
Mathematical Olympiad, Diploma of IInd Degree ("silver medal") |
| 1992
|
|
Inter-Republic
Mathematical Olympiad, Diploma of IIIrd Degree ("bronze medal") |
| |
|
|
| Talks |
|
|
| Nov
2004 |
|
1st Annual New
York Graduate Student Logic Conference, St. Francis College, Brooklyn,
NY |
| Sep
2004 |
|
Theorem
Proving in Higher Order Logics, 17th International Conference, Park
City, UT |
| Mar
2002 |
|
The
PRL Seminar, Cornell University, Ithaca, NY |
| |
|
|
| Academic and Community
Service
|
|
|
| Since
2002 |
|
Organizational
support of Computer Science Colloqium and Logic Colloqium at the
Graduate Center, CUNY |